theorem -- the thing we want to prove Proof say things that the reader (a) will believe are true (b) will not find too tedius ending up with the theorem (start with obvious things -- axioms) 1. Apply Equivalence Rules a | (b | c) b | (a | c) -- assoc, comm !!b | (a | c) -- doule neg !b -> (a | c) -- equiv from table Proof: Consider the formula "A | (B | C)". By the associativity and commutativity of "|", that forumula can be re-written as "B | (A | C)". Using double negation and the equivalence of disjunction and implication, that is the same as "!B -> (A | C)". Thus, "A | (B | C) == !B -> (A | C)". [] Proof: Consider the formula "A | (B | C)". By the associativity and commutativity of "|", that forumula can be re-written as "B | (A | C)". Using our axioms, that is the same as "!B -> (A | C)". Thus, "A | (B | C) == !B -> (A | C)". [] Proof: The formula "A | (B | C)" is equivalent to "!B -> (A | C)" by the basic axioms of equivalence. Thus, "A | (B | C) == !B -> (A | C)". [] Theorem: P -> Q === !P | Q Proof We proceed by a case analysis. Either P is true, or it is false. Case 1: P is true ... Case 2: P is false ... Since the theorem is true in all cases, it is true in general.