Proof Checker
Make sure to save your work often to an external editor.
Reloading this page may clear the proof text.
Proof
Documentation
The proof checker supports the following symbols and reserved words. Reserved words and identifiers are case sensitive.
Logic and Arithmetic:
not and or implies iff forall exists ¬ ∧ ∨ ⇒ ⇔ ∀ ∃
+ * = in ∈ NN ℕ
Rule names:
AndIntro AndElimL AndElimR ∧Intro ∧ElimL ∧ElimR
OrIntroL OrIntroR OrElim ∨IntroL ∨IntroR ∨Elim
ImpliesElim ImpliesIntro ⇒Elim ⇒Intro
IffElimF IffElimB IffIntro ⇔ElimF ⇔ElimB ⇔Intro
ForAllElim ForAllIntro ∀Elim ∀Intro
ExistsElim ExistsIntro ∃Elim ∃Intro
ModusTollens DisjunctiveSyllogism Contradiction
Algebra Repeat
Justifications:
by on with := ↦ forward backward