&_{I} | A, B A & B | &_{E} | A & B A | A & B B | |

∨_{I} | A A ∨ B | B A ∨ B | ∨_{E} | A ∨ B, A ⊃ C, B ⊃ C C | |

⊃_{I} | A* . . B A ⊃ B | ⊃_{E} | A ⊃ B, A B | ||

T_{I} | T | ⊥_{E} | ¬ A* . . ⊥ A | ||

∀_{I} | x * . . A(x) ∀x A(x) | ∀_{E} | ∀x A(x) A(t) | ||

∃_{I} | A(t) ∃x A(x) | ∃_{E} | ∃x A(x) A(y) | ||

=_{I} | t = t | =_{E} | t = s, A(t) A(t//s) |

Note that A ≡ B is a shortcut for (A ⊃ B) & (B ⊃ A),
so we don't need rules for ≡. Also ¬ A is a shortcut for (A ⊃ ⊥).
The rules are divided into direct (simple justification) and indirect (proof and subproof) rules.
Apart from mentioned rules we need for reiteration rule. By changing mentioned ⊥_{E}
to the same-named following rule we will get intuitionistic system.

A A | ⊥_{E} | ⊥ A |