Check Your Proof:
Premises (separate with “,” or “;”):
Conclusion:
Using the checker:
Notation for logic operators
| negation: | ∼ |
| conjunction: | ^ |
| disjunction: | v |
| conditional: | -> |
| biconditional: | <-> |
| universal quantification: | Ax or (Ax) |
| existential quantification: | Ex or (Ex) |
Rule names (full and abbreviated)
| modus ponens | ->E |
| modus tollens | MT |
| modus tollendo ponens | DS |
| double negation | DNE |
| addition | vI |
| adjunction | ^I |
| simplification | ^E |
| bicondition | <->I |
| equivalence | <->E |
| repeat | Rep |
| conditional derivation | ->I |
| reductio ad absurdum | RAA |
| universal instantiation | AE |
| universal derivation | AI |
| existential instantiation | EE |
| existential generalization | EI |
| identity introduction | =I |
| substitution of identicals | =E |
Proof operations
| × | delete this line |
 | add a line below this one |
 | add a new subproof below this line |
 | add a new line below this subproof to the parent subproof |
 | add a new subproof below this subproof to the parent subproof |