Check Your Proof:

Premises (separate with “,” or “;”):


Using the checker:

Notation for logic operators

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 ponensDS
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

This site based on the Open Logic Project proof checker.

Modifications by students and faculty at Cal. State University, Monterey Bay. See Credits for details.

Site Version: 3c4a9c35a5d0c2a5bc0ee80d4a5add8a128103d4