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.