A B ------ [&I] A & B	A & B ------ [&E1] A	A & B ------ [&E2] B
A ------ [+I1] A + B	B ------ [+I2] A + B	A + B A => C B => C ---------------------- [+E] C
F ---- [Efq] A	A A => B --------- [=>E] B	-- A ------- [Raa] A

The introduction implication Rule =>I is not above. It corresponds to a Proof Line begining by the Word therefore.
This rule is defined on the syntax page
The conjunction is written &, the disjonction is written +
I = introduction, E = elimination,
=>E = modus ponens,
Efq = ex falso quodlibet, Raa = reductio ad absurdum
In addition to these rules, we define the negation and the equivalence by
-A = A => F
A <=> B = (A => B) & (B => A)
In a proof, one can replace every Formula by an other Formula equal when we replace the Negations and the Equivalences by their Definitions.

examples | rules | syntax | info | download | home

Last Modified : 29-Oct-2009