| &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 | ||
| TI | 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 | |||