# Further Theorems of Propositional Calculus

name: prophilbert2, module version: 1.00.00, rule version: 1.00.00, original: prophilbert2, author of this module: Michael Meyling

## Description

This module includes proofs of popositional calculus theorems. The following theorems and proofs are adapted from D. Hilbert and W. Ackermann's `Grundzuege der theoretischen Logik' (Berlin 1928, Springer)

## References

This document uses the results of the following documents:

## Content

Negation of a conjunction:

1. Proposition
(
Ø(P Ù Q) ® (ØP Ú ØQ))     (hilb18)

Proof:
 1 (ØØP ® P) add proposition hilb6 2 (ØØQ ® Q) replace proposition variable P by Q in 1 3 (ØØ(ØP Ú ØQ) ® (ØP Ú ØQ)) replace proposition variable Q by (ØP Ú ØQ) in 2 4 (Ø(P Ù Q) ® (ØP Ú ØQ)) reverse abbreviation and in 3 at occurence 1 qed

The reverse of a negation of a conjunction:

2. Proposition
((
ØP Ú ØQ) ® Ø(P Ù Q))     (hilb19)

Proof:
 1 (P ® ØØP) add proposition hilb5 2 (Q ® ØØQ) replace proposition variable P by Q in 1 3 ((ØP Ú ØQ) ® ØØ(ØP Ú ØQ)) replace proposition variable Q by (ØP Ú ØQ) in 2 4 ((ØP Ú ØQ) ® Ø(P Ù Q)) reverse abbreviation and in 3 at occurence 1 qed

Negation of a disjunction:

3. Proposition
(
Ø(P Ú Q) ® (ØP Ù ØQ))     (hilb20)

Proof:
 1 (ØØP ® P) add proposition hilb6 2 (ØØQ ® Q) replace proposition variable P by Q in 1 3 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 4 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 3 5 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 4 6 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 5 7 ((D ® C) ® ((Q Ú D) ® (Q Ú C))) replace proposition variable B by Q in 6 8 ((D ® P) ® ((Q Ú D) ® (Q Ú P))) replace proposition variable C by P in 7 9 ((ØØP ® P) ® ((Q Ú ØØP) ® (Q Ú P))) replace proposition variable D by ØØP in 8 10 ((Q Ú ØØP) ® (Q Ú P)) modus ponens with 1, 9 11 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 12 ((P Ú A) ® (A Ú P)) replace proposition variable Q by A in 11 13 ((B Ú A) ® (A Ú B)) replace proposition variable P by B in 12 14 ((B Ú P) ® (P Ú B)) replace proposition variable A by P in 13 15 ((Q Ú P) ® (P Ú Q)) replace proposition variable B by Q in 14 16 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1 17 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 16 18 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 17 19 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 18 20 ((D ® C) ® (((Q Ú ØØP) ® D) ® ((Q Ú ØØP) ® C))) replace proposition variable B by (Q Ú ØØP) in 19 21 ((D ® (P Ú Q)) ® (((Q Ú ØØP) ® D) ® ((Q Ú ØØP) ® (P Ú Q)))) replace proposition variable C by (P Ú Q) in 20 22 (((Q Ú P) ® (P Ú Q)) ® (((Q Ú ØØP) ® (Q Ú P)) ® ((Q Ú ØØP) ® (P Ú Q)))) replace proposition variable D by (Q Ú P) in 21 23 (((Q Ú ØØP) ® (Q Ú P)) ® ((Q Ú ØØP) ® (P Ú Q))) modus ponens with 15, 22 24 ((Q Ú ØØP) ® (P Ú Q)) modus ponens with 10, 23 25 ((B Ú Q) ® (Q Ú B)) replace proposition variable A by Q in 13 26 ((ØØP Ú Q) ® (Q Ú ØØP)) replace proposition variable B by ØØP in 25 27 ((D ® C) ® (((ØØP Ú Q) ® D) ® ((ØØP Ú Q) ® C))) replace proposition variable B by (ØØP Ú Q) in 19 28 ((D ® (P Ú Q)) ® (((ØØP Ú Q) ® D) ® ((ØØP Ú Q) ® (P Ú Q)))) replace proposition variable C by (P Ú Q) in 27 29 (((Q Ú ØØP) ® (P Ú Q)) ® (((ØØP Ú Q) ® (Q Ú ØØP)) ® ((ØØP Ú Q) ® (P Ú Q)))) replace proposition variable D by (Q Ú ØØP) in 28 30 (((ØØP Ú Q) ® (Q Ú ØØP)) ® ((ØØP Ú Q) ® (P Ú Q))) modus ponens with 24, 29 31 ((ØØP Ú Q) ® (P Ú Q)) modus ponens with 26, 30 32 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7 33 ((P ® A) ® (ØA ® ØP)) replace proposition variable Q by A in 32 34 ((B ® A) ® (ØA ® ØB)) replace proposition variable P by B in 33 35 ((B ® (P Ú Q)) ® (Ø(P Ú Q) ® ØB)) replace proposition variable A by (P Ú Q) in 34 36 (((ØØP Ú Q) ® (P Ú Q)) ® (Ø(P Ú Q) ® Ø(ØØP Ú Q))) replace proposition variable B by (ØØP Ú Q) in 35 37 (Ø(P Ú Q) ® Ø(ØØP Ú Q)) modus ponens with 31, 36 38 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1 39 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2 40 ((P ® A) ® (ØP Ú A)) replace proposition variable Q by A in 38 41 ((B ® A) ® (ØB Ú A)) replace proposition variable P by B in 40 42 ((ØP Ú A) ® (P ® A)) replace proposition variable Q by A in 39 43 ((ØB Ú A) ® (B ® A)) replace proposition variable P by B in 42 44 ((D ® C) ® ((ØØP Ú D) ® (ØØP Ú C))) replace proposition variable B by ØØP in 6 45 ((D ® Q) ® ((ØØP Ú D) ® (ØØP Ú Q))) replace proposition variable C by Q in 44 46 ((ØØQ ® Q) ® ((ØØP Ú ØØQ) ® (ØØP Ú Q))) replace proposition variable D by ØØQ in 45 47 ((ØØP Ú ØØQ) ® (ØØP Ú Q)) modus ponens with 2, 46 48 ((B ® (ØØP Ú Q)) ® (Ø(ØØP Ú Q) ® ØB)) replace proposition variable A by (ØØP Ú Q) in 34 49 (((ØØP Ú ØØQ) ® (ØØP Ú Q)) ® (Ø(ØØP Ú Q) ® Ø(ØØP Ú ØØQ))) replace proposition variable B by (ØØP Ú ØØQ) in 48 50 (Ø(ØØP Ú Q) ® Ø(ØØP Ú ØØQ)) modus ponens with 47, 49 51 ((D ® C) ® ((ØØ(P Ú Q) Ú D) ® (ØØ(P Ú Q) Ú C))) replace proposition variable B by ØØ(P Ú Q) in 6 52 ((D ® Ø(ØØP Ú ØØQ)) ® ((ØØ(P Ú Q) Ú D) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)))) replace proposition variable C by Ø(ØØP Ú ØØQ) in 51 53 ((Ø(ØØP Ú Q) ® Ø(ØØP Ú ØØQ)) ® ((ØØ(P Ú Q) Ú Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)))) replace proposition variable D by Ø(ØØP Ú Q) in 52 54 ((ØØ(P Ú Q) Ú Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) modus ponens with 50, 53 55 ((B ® Ø(ØØP Ú Q)) ® (ØB Ú Ø(ØØP Ú Q))) replace proposition variable A by Ø(ØØP Ú Q) in 41 56 ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú Q))) replace proposition variable B by Ø(P Ú Q) in 55 57 ((D ® C) ® (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® D) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® C))) replace proposition variable B by (Ø(P Ú Q) ® Ø(ØØP Ú Q)) in 19 58 ((D ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) ® (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® D) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))))) replace proposition variable C by (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)) in 57 59 (((ØØ(P Ú Q) Ú Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) ® (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú Q))) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))))) replace proposition variable D by (ØØ(P Ú Q) Ú Ø(ØØP Ú Q)) in 58 60 (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú Q))) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)))) modus ponens with 54, 59 61 ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) modus ponens with 56, 60 62 ((ØB Ú Ø(ØØP Ú ØØQ)) ® (B ® Ø(ØØP Ú ØØQ))) replace proposition variable A by Ø(ØØP Ú ØØQ) in 43 63 ((ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)) ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ))) replace proposition variable B by Ø(P Ú Q) in 62 64 ((D ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ))) ® (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® D) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ))))) replace proposition variable C by (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ)) in 57 65 (((ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)) ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ))) ® (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ))))) replace proposition variable D by (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)) in 64 66 (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ)))) modus ponens with 63, 65 67 ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ))) modus ponens with 61, 66 68 (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ)) modus ponens with 37, 67 69 (Ø(P Ú Q) ® (ØP Ù ØQ)) reverse abbreviation and in 68 at occurence 1 qed

Reverse of a negation of a disjunction:

4. Proposition
((
ØP Ù ØQ) ® Ø(P Ú Q))     (hilb21)

Proof:
 1 (P ® ØØP) add proposition hilb5 2 (Q ® ØØQ) replace proposition variable P by Q in 1 3 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 4 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 3 5 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 4 6 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 5 7 ((D ® C) ® ((Q Ú D) ® (Q Ú C))) replace proposition variable B by Q in 6 8 ((D ® ØØP) ® ((Q Ú D) ® (Q Ú ØØP))) replace proposition variable C by ØØP in 7 9 ((P ® ØØP) ® ((Q Ú P) ® (Q Ú ØØP))) replace proposition variable D by P in 8 10 ((Q Ú P) ® (Q Ú ØØP)) modus ponens with 1, 9 11 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 12 ((P Ú A) ® (A Ú P)) replace proposition variable Q by A in 11 13 ((B Ú A) ® (A Ú B)) replace proposition variable P by B in 12 14 ((B Ú ØØP) ® (ØØP Ú B)) replace proposition variable A by ØØP in 13 15 ((Q Ú ØØP) ® (ØØP Ú Q)) replace proposition variable B by Q in 14 16 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1 17 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 16 18 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 17 19 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 18 20 ((D ® C) ® (((Q Ú P) ® D) ® ((Q Ú P) ® C))) replace proposition variable B by (Q Ú P) in 19 21 ((D ® (ØØP Ú Q)) ® (((Q Ú P) ® D) ® ((Q Ú P) ® (ØØP Ú Q)))) replace proposition variable C by (ØØP Ú Q) in 20 22 (((Q Ú ØØP) ® (ØØP Ú Q)) ® (((Q Ú P) ® (Q Ú ØØP)) ® ((Q Ú P) ® (ØØP Ú Q)))) replace proposition variable D by (Q Ú ØØP) in 21 23 (((Q Ú P) ® (Q Ú ØØP)) ® ((Q Ú P) ® (ØØP Ú Q))) modus ponens with 15, 22 24 ((Q Ú P) ® (ØØP Ú Q)) modus ponens with 10, 23 25 ((D ® C) ® (((P Ú Q) ® D) ® ((P Ú Q) ® C))) replace proposition variable B by (P Ú Q) in 19 26 ((D ® (ØØP Ú Q)) ® (((P Ú Q) ® D) ® ((P Ú Q) ® (ØØP Ú Q)))) replace proposition variable C by (ØØP Ú Q) in 25 27 (((Q Ú P) ® (ØØP Ú Q)) ® (((P Ú Q) ® (Q Ú P)) ® ((P Ú Q) ® (ØØP Ú Q)))) replace proposition variable D by (Q Ú P) in 26 28 (((P Ú Q) ® (Q Ú P)) ® ((P Ú Q) ® (ØØP Ú Q))) modus ponens with 24, 27 29 ((P Ú Q) ® (ØØP Ú Q)) modus ponens with 11, 28 30 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7 31 ((P ® A) ® (ØA ® ØP)) replace proposition variable Q by A in 30 32 ((B ® A) ® (ØA ® ØB)) replace proposition variable P by B in 31 33 ((B ® (ØØP Ú Q)) ® (Ø(ØØP Ú Q) ® ØB)) replace proposition variable A by (ØØP Ú Q) in 32 34 (((P Ú Q) ® (ØØP Ú Q)) ® (Ø(ØØP Ú Q) ® Ø(P Ú Q))) replace proposition variable B by (P Ú Q) in 33 35 (Ø(ØØP Ú Q) ® Ø(P Ú Q)) modus ponens with 29, 34 36 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1 37 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2 38 ((B Ú Ø(P Ú Q)) ® (Ø(P Ú Q) Ú B)) replace proposition variable A by Ø(P Ú Q) in 13 39 ((P ® A) ® (ØP Ú A)) replace proposition variable Q by A in 36 40 ((B ® A) ® (ØB Ú A)) replace proposition variable P by B in 39 41 ((B ® Ø(P Ú Q)) ® (ØB Ú Ø(P Ú Q))) replace proposition variable A by Ø(P Ú Q) in 40 42 ((ØP Ú A) ® (P ® A)) replace proposition variable Q by A in 37 43 ((ØB Ú A) ® (B ® A)) replace proposition variable P by B in 42 44 ((ØB Ú Ø(P Ú Q)) ® (B ® Ø(P Ú Q))) replace proposition variable A by Ø(P Ú Q) in 43 45 ((D ® C) ® ((ØØP Ú D) ® (ØØP Ú C))) replace proposition variable B by ØØP in 6 46 ((D ® ØØQ) ® ((ØØP Ú D) ® (ØØP Ú ØØQ))) replace proposition variable C by ØØQ in 45 47 ((Q ® ØØQ) ® ((ØØP Ú Q) ® (ØØP Ú ØØQ))) replace proposition variable D by Q in 46 48 ((ØØP Ú Q) ® (ØØP Ú ØØQ)) modus ponens with 2, 47 49 ((B ® (ØØP Ú ØØQ)) ® (Ø(ØØP Ú ØØQ) ® ØB)) replace proposition variable A by (ØØP Ú ØØQ) in 32 50 (((ØØP Ú Q) ® (ØØP Ú ØØQ)) ® (Ø(ØØP Ú ØØQ) ® Ø(ØØP Ú Q))) replace proposition variable B by (ØØP Ú Q) in 49 51 (Ø(ØØP Ú ØØQ) ® Ø(ØØP Ú Q)) modus ponens with 48, 50 52 ((B ® Ø(ØØP Ú Q)) ® (ØØ(ØØP Ú Q) ® ØB)) replace proposition variable A by Ø(ØØP Ú Q) in 32 53 ((Ø(ØØP Ú ØØQ) ® Ø(ØØP Ú Q)) ® (ØØ(ØØP Ú Q) ® ØØ(ØØP Ú ØØQ))) replace proposition variable B by Ø(ØØP Ú ØØQ) in 52 54 (ØØ(ØØP Ú Q) ® ØØ(ØØP Ú ØØQ)) modus ponens with 51, 53 55 ((D ® C) ® ((Ø(P Ú Q) Ú D) ® (Ø(P Ú Q) Ú C))) replace proposition variable B by Ø(P Ú Q) in 6 56 ((D ® ØØ(ØØP Ú ØØQ)) ® ((Ø(P Ú Q) Ú D) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ)))) replace proposition variable C by ØØ(ØØP Ú ØØQ) in 55 57 ((ØØ(ØØP Ú Q) ® ØØ(ØØP Ú ØØQ)) ® ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ)))) replace proposition variable D by ØØ(ØØP Ú Q) in 56 58 ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ))) modus ponens with 54, 57 59 ((B Ú ØØ(ØØP Ú ØØQ)) ® (ØØ(ØØP Ú ØØQ) Ú B)) replace proposition variable A by ØØ(ØØP Ú ØØQ) in 13 60 ((Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) replace proposition variable B by Ø(P Ú Q) in 59 61 ((D ® C) ® (((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® D) ® ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® C))) replace proposition variable B by (Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) in 19 62 ((D ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) ® (((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® D) ® ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))))) replace proposition variable C by (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)) in 61 63 (((Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) ® (((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ))) ® ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))))) replace proposition variable D by (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ)) in 62 64 (((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ))) ® ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)))) modus ponens with 60, 63 65 ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) modus ponens with 58, 64 66 ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú Q))) replace proposition variable B by ØØ(ØØP Ú Q) in 38 67 ((D ® C) ® (((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® D) ® ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® C))) replace proposition variable B by (ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) in 19 68 ((D ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) ® (((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® D) ® ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))))) replace proposition variable C by (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)) in 67 69 (((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) ® (((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú Q))) ® ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))))) replace proposition variable D by (Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) in 68 70 (((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú Q))) ® ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)))) modus ponens with 65, 69 71 ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) modus ponens with 66, 70 72 ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú Q) Ú Ø(P Ú Q))) replace proposition variable B by Ø(ØØP Ú Q) in 41 73 ((D ® C) ® (((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® D) ® ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® C))) replace proposition variable B by (Ø(ØØP Ú Q) ® Ø(P Ú Q)) in 19 74 ((D ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) ® (((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® D) ® ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))))) replace proposition variable C by (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)) in 73 75 (((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) ® (((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú Q) Ú Ø(P Ú Q))) ® ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))))) replace proposition variable D by (ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) in 74 76 (((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú Q) Ú Ø(P Ú Q))) ® ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)))) modus ponens with 71, 75 77 ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) modus ponens with 72, 76 78 ((ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)) ® (Ø(ØØP Ú ØØQ) ® Ø(P Ú Q))) replace proposition variable B by Ø(ØØP Ú ØØQ) in 44 79 ((D ® (Ø(ØØP Ú ØØQ) ® Ø(P Ú Q))) ® (((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® D) ® ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (Ø(ØØP Ú ØØQ) ® Ø(P Ú Q))))) replace proposition variable C by (Ø(ØØP Ú ØØQ) ® Ø(P Ú Q)) in 73 80 (((ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)) ® (Ø(ØØP Ú ØØQ) ® Ø(P Ú Q))) ® (((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) ® ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (Ø(ØØP Ú ØØQ) ® Ø(P Ú Q))))) replace proposition variable D by (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)) in 79 81 (((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) ® ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (Ø(ØØP Ú ØØQ) ® Ø(P Ú Q)))) modus ponens with 78, 80 82 ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (Ø(ØØP Ú ØØQ) ® Ø(P Ú Q))) modus ponens with 77, 81 83 (Ø(ØØP Ú ØØQ) ® Ø(P Ú Q)) modus ponens with 35, 82 84 ((ØP Ù ØQ) ® Ø(P Ú Q)) reverse abbreviation and in 83 at occurence 1 qed

The Conjunction is commutative:

5. Proposition
((P
Ù Q) ® (Q Ù P))     (hilb22)

Proof:
 1 (P ® P) add proposition hilb2 2 (Q ® Q) replace proposition variable P by Q in 1 3 ((P Ù Q) ® (P Ù Q)) replace proposition variable Q by (P Ù Q) in 2 4 ((P Ù Q) ® Ø(ØP Ú ØQ)) use abbreviation and in 3 at occurence 2 5 ((Q Ú P) ® (P Ú Q)) add proposition hilb10 6 ((A Ú P) ® (P Ú A)) replace proposition variable Q by A in 5 7 ((A Ú B) ® (B Ú A)) replace proposition variable P by B in 6 8 ((ØQ Ú B) ® (B Ú ØQ)) replace proposition variable A by ØQ in 7 9 ((ØQ Ú ØP) ® (ØP Ú ØQ)) replace proposition variable B by ØP in 8 10 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7 11 ((P ® A) ® (ØA ® ØP)) replace proposition variable Q by A in 10 12 ((B ® A) ® (ØA ® ØB)) replace proposition variable P by B in 11 13 ((B ® (ØP Ú ØQ)) ® (Ø(ØP Ú ØQ) ® ØB)) replace proposition variable A by (ØP Ú ØQ) in 12 14 (((ØQ Ú ØP) ® (ØP Ú ØQ)) ® (Ø(ØP Ú ØQ) ® Ø(ØQ Ú ØP))) replace proposition variable B by (ØQ Ú ØP) in 13 15 (Ø(ØP Ú ØQ) ® Ø(ØQ Ú ØP)) modus ponens with 9, 14 16 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1 17 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2 18 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 19 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 18 20 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 19 21 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 20 22 ((D ® C) ® ((Ø(P Ù Q) Ú D) ® (Ø(P Ù Q) Ú C))) replace proposition variable B by Ø(P Ù Q) in 21 23 ((D ® Ø(ØQ Ú ØP)) ® ((Ø(P Ù Q) Ú D) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)))) replace proposition variable C by Ø(ØQ Ú ØP) in 22 24 ((Ø(ØP Ú ØQ) ® Ø(ØQ Ú ØP)) ® ((Ø(P Ù Q) Ú Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)))) replace proposition variable D by Ø(ØP Ú ØQ) in 23 25 ((Ø(P Ù Q) Ú Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) modus ponens with 15, 24 26 ((P ® A) ® (ØP Ú A)) replace proposition variable Q by A in 16 27 ((B ® A) ® (ØB Ú A)) replace proposition variable P by B in 26 28 ((B ® Ø(ØP Ú ØQ)) ® (ØB Ú Ø(ØP Ú ØQ))) replace proposition variable A by Ø(ØP Ú ØQ) in 27 29 (((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØP Ú ØQ))) replace proposition variable B by (P Ù Q) in 28 30 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1 31 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 30 32 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 31 33 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 32 34 ((D ® C) ® ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® D) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® C))) replace proposition variable B by ((P Ù Q) ® Ø(ØP Ú ØQ)) in 33 35 ((D ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) ® ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® D) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))))) replace proposition variable C by (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)) in 34 36 (((Ø(P Ù Q) Ú Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) ® ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØP Ú ØQ))) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))))) replace proposition variable D by (Ø(P Ù Q) Ú Ø(ØP Ú ØQ)) in 35 37 ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØP Ú ØQ))) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)))) modus ponens with 25, 36 38 (((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) modus ponens with 29, 37 39 ((ØP Ú A) ® (P ® A)) replace proposition variable Q by A in 17 40 ((ØB Ú A) ® (B ® A)) replace proposition variable P by B in 39 41 ((ØB Ú Ø(ØQ Ú ØP)) ® (B ® Ø(ØQ Ú ØP))) replace proposition variable A by Ø(ØQ Ú ØP) in 40 42 ((Ø(P Ù Q) Ú Ø(ØQ Ú ØP)) ® ((P Ù Q) ® Ø(ØQ Ú ØP))) replace proposition variable B by (P Ù Q) in 41 43 ((D ® ((P Ù Q) ® Ø(ØQ Ú ØP))) ® ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® D) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® ((P Ù Q) ® Ø(ØQ Ú ØP))))) replace proposition variable C by ((P Ù Q) ® Ø(ØQ Ú ØP)) in 34 44 (((Ø(P Ù Q) Ú Ø(ØQ Ú ØP)) ® ((P Ù Q) ® Ø(ØQ Ú ØP))) ® ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® ((P Ù Q) ® Ø(ØQ Ú ØP))))) replace proposition variable D by (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)) in 43 45 ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® ((P Ù Q) ® Ø(ØQ Ú ØP)))) modus ponens with 42, 44 46 (((P Ù Q) ® Ø(ØP Ú ØQ)) ® ((P Ù Q) ® Ø(ØQ Ú ØP))) modus ponens with 38, 45 47 ((P Ù Q) ® Ø(ØQ Ú ØP)) modus ponens with 4, 46 48 ((P Ù Q) ® (Q Ù P)) reverse abbreviation and in 47 at occurence 1 qed

A technical lemma that is simular to the previous one:

6. Proposition
((Q
Ù P) ® (P Ù Q))     (hilb23)

Proof:
 1 ((P Ù Q) ® (Q Ù P)) add proposition hilb22 2 ((P Ù A) ® (A Ù P)) replace proposition variable Q by A in 1 3 ((B Ù A) ® (A Ù B)) replace proposition variable P by B in 2 4 ((B Ù P) ® (P Ù B)) replace proposition variable A by P in 3 5 ((Q Ù P) ® (P Ù Q)) replace proposition variable B by Q in 4 qed

Reduction of a conjunction:

7. Proposition
((P
Ù Q) ® P)     (hilb24)

Proof:
 1 (P ® (P Ú Q)) add axiom axiom2 2 (P ® (P Ú A)) replace proposition variable Q by A in 1 3 (B ® (B Ú A)) replace proposition variable P by B in 2 4 (B ® (B Ú ØQ)) replace proposition variable A by ØQ in 3 5 (ØP ® (ØP Ú ØQ)) replace proposition variable B by ØP in 4 6 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7 7 ((P ® A) ® (ØA ® ØP)) replace proposition variable Q by A in 6 8 ((B ® A) ® (ØA ® ØB)) replace proposition variable P by B in 7 9 ((B ® (ØP Ú ØQ)) ® (Ø(ØP Ú ØQ) ® ØB)) replace proposition variable A by (ØP Ú ØQ) in 8 10 ((ØP ® (ØP Ú ØQ)) ® (Ø(ØP Ú ØQ) ® ØØP)) replace proposition variable B by ØP in 9 11 (Ø(ØP Ú ØQ) ® ØØP) modus ponens with 5, 10 12 ((P Ù Q) ® ØØP) reverse abbreviation and in 11 at occurence 1 13 (ØØP ® P) add proposition hilb6 14 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1 15 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2 16 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 17 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 16 18 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 17 19 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 18 20 ((D ® C) ® ((Ø(P Ù Q) Ú D) ® (Ø(P Ù Q) Ú C))) replace proposition variable B by Ø(P Ù Q) in 19 21 ((D ® P) ® ((Ø(P Ù Q) Ú D) ® (Ø(P Ù Q) Ú P))) replace proposition variable C by P in 20 22 ((ØØP ® P) ® ((Ø(P Ù Q) Ú ØØP) ® (Ø(P Ù Q) Ú P))) replace proposition variable D by ØØP in 21 23 ((Ø(P Ù Q) Ú ØØP) ® (Ø(P Ù Q) Ú P)) modus ponens with 13, 22 24 ((P ® A) ® (ØP Ú A)) replace proposition variable Q by A in 14 25 ((B ® A) ® (ØB Ú A)) replace proposition variable P by B in 24 26 ((B ® ØØP) ® (ØB Ú ØØP)) replace proposition variable A by ØØP in 25 27 (((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú ØØP)) replace proposition variable B by (P Ù Q) in 26 28 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1 29 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 28 30 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 29 31 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 30 32 ((D ® C) ® ((((P Ù Q) ® ØØP) ® D) ® (((P Ù Q) ® ØØP) ® C))) replace proposition variable B by ((P Ù Q) ® ØØP) in 31 33 ((D ® (Ø(P Ù Q) Ú P)) ® ((((P Ù Q) ® ØØP) ® D) ® (((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú P)))) replace proposition variable C by (Ø(P Ù Q) Ú P) in 32 34 (((Ø(P Ù Q) Ú ØØP) ® (Ø(P Ù Q) Ú P)) ® ((((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú ØØP)) ® (((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú P)))) replace proposition variable D by (Ø(P Ù Q) Ú ØØP) in 33 35 ((((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú ØØP)) ® (((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú P))) modus ponens with 23, 34 36 (((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú P)) modus ponens with 27, 35 37 ((ØP Ú A) ® (P ® A)) replace proposition variable Q by A in 15 38 ((ØB Ú A) ® (B ® A)) replace proposition variable P by B in 37 39 ((ØB Ú P) ® (B ® P)) replace proposition variable A by P in 38 40 ((Ø(P Ù Q) Ú P) ® ((P Ù Q) ® P)) replace proposition variable B by (P Ù Q) in 39 41 ((D ® ((P Ù Q) ® P)) ® ((((P Ù Q) ® ØØP) ® D) ® (((P Ù Q) ® ØØP) ® ((P Ù Q) ® P)))) replace proposition variable C by ((P Ù Q) ® P) in 32 42 (((Ø(P Ù Q) Ú P) ® ((P Ù Q) ® P)) ® ((((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú P)) ® (((P Ù Q) ® ØØP) ® ((P Ù Q) ® P)))) replace proposition variable D by (Ø(P Ù Q) Ú P) in 41 43 ((((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú P)) ® (((P Ù Q) ® ØØP) ® ((P Ù Q) ® P))) modus ponens with 40, 42 44 (((P Ù Q) ® ØØP) ® ((P Ù Q) ® P)) modus ponens with 36, 43 45 ((P Ù Q) ® P) modus ponens with 12, 44 qed

Another form of a reduction of a conjunction:

8. Proposition
((P
Ù Q) ® Q)     (hilb25)

Proof:
 1 ((P Ù Q) ® P) add proposition hilb24 2 ((P Ù A) ® P) replace proposition variable Q by A in 1 3 ((B Ù A) ® B) replace proposition variable P by B in 2 4 ((B Ù P) ® B) replace proposition variable A by P in 3 5 ((Q Ù P) ® Q) replace proposition variable B by Q in 4 6 ((Q Ù P) ® (P Ù Q)) add proposition hilb23 7 ((A Ù P) ® (P Ù A)) replace proposition variable Q by A in 6 8 ((A Ù B) ® (B Ù A)) replace proposition variable P by B in 7 9 ((P Ù B) ® (B Ù P)) replace proposition variable A by P in 8 10 ((P Ù Q) ® (Q Ù P)) replace proposition variable B by Q in 9 11 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1 12 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2 13 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7 14 ((P ® A) ® (ØA ® ØP)) replace proposition variable Q by A in 13 15 ((B ® A) ® (ØA ® ØB)) replace proposition variable P by B in 14 16 ((B ® (Q Ù P)) ® (Ø(Q Ù P) ® ØB)) replace proposition variable A by (Q Ù P) in 15 17 (((P Ù Q) ® (Q Ù P)) ® (Ø(Q Ù P) ® Ø(P Ù Q))) replace proposition variable B by (P Ù Q) in 16 18 (Ø(Q Ù P) ® Ø(P Ù Q)) modus ponens with 10, 17 19 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 20 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 19 21 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 20 22 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 21 23 ((D ® C) ® ((Q Ú D) ® (Q Ú C))) replace proposition variable B by Q in 22 24 ((D ® Ø(P Ù Q)) ® ((Q Ú D) ® (Q Ú Ø(P Ù Q)))) replace proposition variable C by Ø(P Ù Q) in 23 25 ((Ø(Q Ù P) ® Ø(P Ù Q)) ® ((Q Ú Ø(Q Ù P)) ® (Q Ú Ø(P Ù Q)))) replace proposition variable D by Ø(Q Ù P) in 24 26 ((Q Ú Ø(Q Ù P)) ® (Q Ú Ø(P Ù Q))) modus ponens with 18, 25 27 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 28 ((P Ú A) ® (A Ú P)) replace proposition variable Q by A in 27 29 ((B Ú A) ® (A Ú B)) replace proposition variable P by B in 28 30 ((B Ú Ø(P Ù Q)) ® (Ø(P Ù Q) Ú B)) replace proposition variable A by Ø(P Ù Q) in 29 31 ((Q Ú Ø(P Ù Q)) ® (Ø(P Ù Q) Ú Q)) replace proposition variable B by Q in 30 32 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1 33 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 32 34 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 33 35 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 34 36 ((D ® C) ® (((Q Ú Ø(Q Ù P)) ® D) ® ((Q Ú Ø(Q Ù P)) ® C))) replace proposition variable B by (Q Ú Ø(Q Ù P)) in 35 37 ((D ® (Ø(P Ù Q) Ú Q)) ® (((Q Ú Ø(Q Ù P)) ® D) ® ((Q Ú Ø(Q Ù P)) ® (Ø(P Ù Q) Ú Q)))) replace proposition variable C by (Ø(P Ù Q) Ú Q) in 36 38 (((Q Ú Ø(P Ù Q)) ® (Ø(P Ù Q) Ú Q)) ® (((Q Ú Ø(Q Ù P)) ® (Q Ú Ø(P Ù Q))) ® ((Q Ú Ø(Q Ù P)) ® (Ø(P Ù Q) Ú Q)))) replace proposition variable D by (Q Ú Ø(P Ù Q)) in 37 39 (((Q Ú Ø(Q Ù P)) ® (Q Ú Ø(P Ù Q))) ® ((Q Ú Ø(Q Ù P)) ® (Ø(P Ù Q) Ú Q))) modus ponens with 31, 38 40 ((Q Ú Ø(Q Ù P)) ® (Ø(P Ù Q) Ú Q)) modus ponens with 26, 39 41 ((B Ú Q) ® (Q Ú B)) replace proposition variable A by Q in 29 42 ((Ø(Q Ù P) Ú Q) ® (Q Ú Ø(Q Ù P))) replace proposition variable B by Ø(Q Ù P) in 41 43 ((D ® C) ® (((Ø(Q Ù P) Ú Q) ® D) ® ((Ø(Q Ù P) Ú Q) ® C))) replace proposition variable B by (Ø(Q Ù P) Ú Q) in 35 44 ((D ® (Ø(P Ù Q) Ú Q)) ® (((Ø(Q Ù P) Ú Q) ® D) ® ((Ø(Q Ù P) Ú Q) ® (Ø(P Ù Q) Ú Q)))) replace proposition variable C by (Ø(P Ù Q) Ú Q) in 43 45 (((Q Ú Ø(Q Ù P)) ® (Ø(P Ù Q) Ú Q)) ® (((Ø(Q Ù P) Ú Q) ® (Q Ú Ø(Q Ù P))) ® ((Ø(Q Ù P) Ú Q) ® (Ø(P Ù Q) Ú Q)))) replace proposition variable D by (Q Ú Ø(Q Ù P)) in 44 46 (((Ø(Q Ù P) Ú Q) ® (Q Ú Ø(Q Ù P))) ® ((Ø(Q Ù P) Ú Q) ® (Ø(P Ù Q) Ú Q))) modus ponens with 40, 45 47 ((Ø(Q Ù P) Ú Q) ® (Ø(P Ù Q) Ú Q)) modus ponens with 42, 46 48 ((P ® A) ® (ØP Ú A)) replace proposition variable Q by A in 11 49 ((B ® A) ® (ØB Ú A)) replace proposition variable P by B in 48 50 ((B ® Q) ® (ØB Ú Q)) replace proposition variable A by Q in 49 51 (((Q Ù P) ® Q) ® (Ø(Q Ù P) Ú Q)) replace proposition variable B by (Q Ù P) in 50 52 ((D ® C) ® ((((Q Ù P) ® Q) ® D) ® (((Q Ù P) ® Q) ® C))) replace proposition variable B by ((Q Ù P) ® Q) in 35 53 ((D ® (Ø(P Ù Q) Ú Q)) ® ((((Q Ù P) ® Q) ® D) ® (((Q Ù P) ® Q) ® (Ø(P Ù Q) Ú Q)))) replace proposition variable C by (Ø(P Ù Q) Ú Q) in 52 54 (((Ø(Q Ù P) Ú Q) ® (Ø(P Ù Q) Ú Q)) ® ((((Q Ù P) ® Q) ® (Ø(Q Ù P) Ú Q)) ® (((Q Ù P) ® Q) ® (Ø(P Ù Q) Ú Q)))) replace proposition variable D by (Ø(Q Ù P) Ú Q) in 53 55 ((((Q Ù P) ® Q) ® (Ø(Q Ù P) Ú Q)) ® (((Q Ù P) ® Q) ® (Ø(P Ù Q) Ú Q))) modus ponens with 47, 54 56 (((Q Ù P) ® Q) ® (Ø(P Ù Q) Ú Q)) modus ponens with 51, 55 57 ((ØP Ú A) ® (P ® A)) replace proposition variable Q by A in 12 58 ((ØB Ú A) ® (B ® A)) replace proposition variable P by B in 57 59 ((ØB Ú Q) ® (B ® Q)) replace proposition variable A by Q in 58 60 ((Ø(P Ù Q) Ú Q) ® ((P Ù Q) ® Q)) replace proposition variable B by (P Ù Q) in 59 61 ((D ® ((P Ù Q) ® Q)) ® ((((Q Ù P) ® Q) ® D) ® (((Q Ù P) ® Q) ® ((P Ù Q) ® Q)))) replace proposition variable C by ((P Ù Q) ® Q) in 52 62 (((Ø(P Ù Q) Ú Q) ® ((P Ù Q) ® Q)) ® ((((Q Ù P) ® Q) ® (Ø(P Ù Q) Ú Q)) ® (((Q Ù P) ® Q) ® ((P Ù Q) ® Q)))) replace proposition variable D by (Ø(P Ù Q) Ú Q) in 61 63 ((((Q Ù P) ® Q) ® (Ø(P Ù Q) Ú Q)) ® (((Q Ù P) ® Q) ® ((P Ù Q) ® Q))) modus ponens with 60, 62 64 (((Q Ù P) ® Q) ® ((P Ù Q) ® Q)) modus ponens with 56, 63 65 ((P Ù Q) ® Q) modus ponens with 5, 64 qed

The conjunction is associative too (first implication):

9. Proposition
((P
Ù (Q Ù A)) ® ((P Ù Q) Ù A))     (hilb26)

Proof:
 1 (((P Ú Q) Ú A) ® (P Ú (Q Ú A))) add proposition hilb15 2 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7 3 ((P ® A) ® (ØA ® ØP)) replace proposition variable Q by A in 2 4 ((B ® A) ® (ØA ® ØB)) replace proposition variable P by B in 3 5 ((B ® (P Ú (Q Ú A))) ® (Ø(P Ú (Q Ú A)) ® ØB)) replace proposition variable A by (P Ú (Q Ú A)) in 4 6 ((((P Ú Q) Ú A) ® (P Ú (Q Ú A))) ® (Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A))) replace proposition variable B by ((P Ú Q) Ú A) in 5 7 (Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) modus ponens with 1, 6 8 (P ® ØØP) add proposition hilb5 9 (B ® ØØB) replace proposition variable P by B in 8 10 ((Q Ú A) ® ØØ(Q Ú A)) replace proposition variable B by (Q Ú A) in 9 11 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 12 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 11 13 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 12 14 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 13 15 ((D ® C) ® ((P Ú D) ® (P Ú C))) replace proposition variable B by P in 14 16 ((D ® ØØ(Q Ú A)) ® ((P Ú D) ® (P Ú ØØ(Q Ú A)))) replace proposition variable C by ØØ(Q Ú A) in 15 17 (((Q Ú A) ® ØØ(Q Ú A)) ® ((P Ú (Q Ú A)) ® (P Ú ØØ(Q Ú A)))) replace proposition variable D by (Q Ú A) in 16 18 ((P Ú (Q Ú A)) ® (P Ú ØØ(Q Ú A))) modus ponens with 10, 17 19 ((P ® B) ® (ØB ® ØP)) replace proposition variable Q by B in 2 20 ((C ® B) ® (ØB ® ØC)) replace proposition variable P by C in 19 21 ((C ® (P Ú ØØ(Q Ú A))) ® (Ø(P Ú ØØ(Q Ú A)) ® ØC)) replace proposition variable B by (P Ú ØØ(Q Ú A)) in 20 22 (((P Ú (Q Ú A)) ® (P Ú ØØ(Q Ú A))) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø(P Ú (Q Ú A)))) replace proposition variable C by (P Ú (Q Ú A)) in 21 23 (Ø(P Ú ØØ(Q Ú A)) ® Ø(P Ú (Q Ú A))) modus ponens with 18, 22 24 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1 25 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2 26 ((C ® Ø(P Ú (Q Ú A))) ® (ØØ(P Ú (Q Ú A)) ® ØC)) replace proposition variable B by Ø(P Ú (Q Ú A)) in 20 27 ((Ø(P Ú ØØ(Q Ú A)) ® Ø(P Ú (Q Ú A))) ® (ØØ(P Ú (Q Ú A)) ® ØØ(P Ú ØØ(Q Ú A)))) replace proposition variable C by Ø(P Ú ØØ(Q Ú A)) in 26 28 (ØØ(P Ú (Q Ú A)) ® ØØ(P Ú ØØ(Q Ú A))) modus ponens with 23, 27 29 ((D ® C) ® ((Ø((P Ú Q) Ú A) Ú D) ® (Ø((P Ú Q) Ú A) Ú C))) replace proposition variable B by Ø((P Ú Q) Ú A) in 14 30 ((D ® ØØ(P Ú ØØ(Q Ú A))) ® ((Ø((P Ú Q) Ú A) Ú D) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))))) replace proposition variable C by ØØ(P Ú ØØ(Q Ú A)) in 29 31 ((ØØ(P Ú (Q Ú A)) ® ØØ(P Ú ØØ(Q Ú A))) ® ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))))) replace proposition variable D by ØØ(P Ú (Q Ú A)) in 30 32 ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A)))) modus ponens with 28, 31 33 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 34 ((P Ú B) ® (B Ú P)) replace proposition variable Q by B in 33 35 ((C Ú B) ® (B Ú C)) replace proposition variable P by C in 34 36 ((C Ú ØØ(P Ú ØØ(Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú C)) replace proposition variable B by ØØ(P Ú ØØ(Q Ú A)) in 35 37 ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) replace proposition variable C by Ø((P Ú Q) Ú A) in 36 38 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1 39 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 38 40 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 39 41 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 40 42 ((D ® C) ® (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® D) ® ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® C))) replace proposition variable B by (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) in 41 43 ((D ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® D) ® ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) replace proposition variable C by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 42 44 (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A)))) ® ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) replace proposition variable D by (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))) in 43 45 (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A)))) ® ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)))) modus ponens with 37, 44 46 ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) modus ponens with 32, 45 47 ((C Ú Ø((P Ú Q) Ú A)) ® (Ø((P Ú Q) Ú A) Ú C)) replace proposition variable B by Ø((P Ú Q) Ú A) in 35 48 ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A)))) replace proposition variable C by ØØ(P Ú (Q Ú A)) in 47 49 ((D ® C) ® (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® D) ® ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® C))) replace proposition variable B by (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 41 50 ((D ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® D) ® ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) replace proposition variable C by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 49 51 (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A)))) ® ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) replace proposition variable D by (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) in 50 52 (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A)))) ® ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)))) modus ponens with 46, 51 53 ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) modus ponens with 48, 52 54 ((P ® B) ® (ØP Ú B)) replace proposition variable Q by B in 24 55 ((C ® B) ® (ØC Ú B)) replace proposition variable P by C in 54 56 ((C ® Ø((P Ú Q) Ú A)) ® (ØC Ú Ø((P Ú Q) Ú A))) replace proposition variable B by Ø((P Ú Q) Ú A) in 55 57 ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A))) replace proposition variable C by Ø(P Ú (Q Ú A)) in 56 58 ((D ® C) ® (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® D) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® C))) replace proposition variable B by (Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) in 41 59 ((D ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® D) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) replace proposition variable C by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 58 60 (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) replace proposition variable D by (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 59 61 (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)))) modus ponens with 53, 60 62 ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) modus ponens with 57, 61 63 ((ØP Ú B) ® (P ® B)) replace proposition variable Q by B in 25 64 ((ØC Ú B) ® (C ® B)) replace proposition variable P by C in 63 65 ((ØC Ú Ø((P Ú Q) Ú A)) ® (C ® Ø((P Ú Q) Ú A))) replace proposition variable B by Ø((P Ú Q) Ú A) in 64 66 ((ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A))) replace proposition variable C by Ø(P Ú ØØ(Q Ú A)) in 65 67 ((D ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A))) ® (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® D) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A))))) replace proposition variable C by (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) in 58 68 (((ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A))) ® (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A))))) replace proposition variable D by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 67 69 (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)))) modus ponens with 66, 68 70 ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A))) modus ponens with 62, 69 71 (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) modus ponens with 7, 70 72 (ØØP ® P) add proposition hilb6 73 (ØØA ® A) replace proposition variable P by A in 72 74 (ØØ(P Ú Q) ® (P Ú Q)) replace proposition variable A by (P Ú Q) in 73 75 ((D ® C) ® ((A Ú D) ® (A Ú C))) replace proposition variable B by A in 14 76 ((D ® (P Ú Q)) ® ((A Ú D) ® (A Ú (P Ú Q)))) replace proposition variable C by (P Ú Q) in 75 77 ((ØØ(P Ú Q) ® (P Ú Q)) ® ((A Ú ØØ(P Ú Q)) ® (A Ú (P Ú Q)))) replace proposition variable D by ØØ(P Ú Q) in 76 78 ((A Ú ØØ(P Ú Q)) ® (A Ú (P Ú Q))) modus ponens with 74, 77 79 ((C Ú (P Ú Q)) ® ((P Ú Q) Ú C)) replace proposition variable B by (P Ú Q) in 35 80 ((A Ú (P Ú Q)) ® ((P Ú Q) Ú A)) replace proposition variable C by A in 79 81 ((D ® C) ® (((A Ú ØØ(P Ú Q)) ® D) ® ((A Ú ØØ(P Ú Q)) ® C))) replace proposition variable B by (A Ú ØØ(P Ú Q)) in 41 82 ((D ® ((P Ú Q) Ú A)) ® (((A Ú ØØ(P Ú Q)) ® D) ® ((A Ú ØØ(P Ú Q)) ® ((P Ú Q) Ú A)))) replace proposition variable C by ((P Ú Q) Ú A) in 81 83 (((A Ú (P Ú Q)) ® ((P Ú Q) Ú A)) ® (((A Ú ØØ(P Ú Q)) ® (A Ú (P Ú Q))) ® ((A Ú ØØ(P Ú Q)) ® ((P Ú Q) Ú A)))) replace proposition variable D by (A Ú (P Ú Q)) in 82 84 (((A Ú ØØ(P Ú Q)) ® (A Ú (P Ú Q))) ® ((A Ú ØØ(P Ú Q)) ® ((P Ú Q) Ú A))) modus ponens with 80, 83 85 ((A Ú ØØ(P Ú Q)) ® ((P Ú Q) Ú A)) modus ponens with 78, 84 86 ((C Ú A) ® (A Ú C)) replace proposition variable B by A in 35 87 ((ØØ(P Ú Q) Ú A) ® (A Ú ØØ(P Ú Q))) replace proposition variable C by ØØ(P Ú Q) in 86 88 ((D ® C) ® (((ØØ(P Ú Q) Ú A) ® D) ® ((ØØ(P Ú Q) Ú A) ® C))) replace proposition variable B by (ØØ(P Ú Q) Ú A) in 41 89 ((D ® ((P Ú Q) Ú A)) ® (((ØØ(P Ú Q) Ú A) ® D) ® ((ØØ(P Ú Q) Ú A) ® ((P Ú Q) Ú A)))) replace proposition variable C by ((P Ú Q) Ú A) in 88 90 (((A Ú ØØ(P Ú Q)) ® ((P Ú Q) Ú A)) ® (((ØØ(P Ú Q) Ú A) ® (A Ú ØØ(P Ú Q))) ® ((ØØ(P Ú Q) Ú A) ® ((P Ú Q) Ú A)))) replace proposition variable D by (A Ú ØØ(P Ú Q)) in 89 91 (((ØØ(P Ú Q) Ú A) ® (A Ú ØØ(P Ú Q))) ® ((ØØ(P Ú Q) Ú A) ® ((P Ú Q) Ú A))) modus ponens with 85, 90 92 ((ØØ(P Ú Q) Ú A) ® ((P Ú Q) Ú A)) modus ponens with 87, 91 93 ((C ® ((P Ú Q) Ú A)) ® (Ø((P Ú Q) Ú A) ® ØC)) replace proposition variable B by ((P Ú Q) Ú A) in 20 94 (((ØØ(P Ú Q) Ú A) ® ((P Ú Q) Ú A)) ® (Ø((P Ú Q) Ú A) ® Ø(ØØ(P Ú Q) Ú A))) replace proposition variable C by (ØØ(P Ú Q) Ú A) in 93 95 (Ø((P Ú Q) Ú A) ® Ø(ØØ(P Ú Q) Ú A)) modus ponens with 92, 94 96 ((D ® C) ® ((ØØ(P Ú ØØ(Q Ú A)) Ú D) ® (ØØ(P Ú ØØ(Q Ú A)) Ú C))) replace proposition variable B by ØØ(P Ú ØØ(Q Ú A)) in 14 97 ((D ® Ø(ØØ(P Ú Q) Ú A)) ® ((ØØ(P Ú ØØ(Q Ú A)) Ú D) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)))) replace proposition variable C by Ø(ØØ(P Ú Q) Ú A) in 96 98 ((Ø((P Ú Q) Ú A) ® Ø(ØØ(P Ú Q) Ú A)) ® ((ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)))) replace proposition variable D by Ø((P Ú Q) Ú A) in 97 99 ((ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))) modus ponens with 95, 98 100 ((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) replace proposition variable C by Ø(P Ú ØØ(Q Ú A)) in 56 101 ((D ® C) ® (((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® D) ® ((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® C))) replace proposition variable B by (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) in 41 102 ((D ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))) ® (((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® D) ® ((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))))) replace proposition variable C by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)) in 101 103 (((ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))) ® (((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® ((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))))) replace proposition variable D by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 102 104 (((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® ((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)))) modus ponens with 99, 103 105 ((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))) modus ponens with 100, 104 106 ((ØC Ú Ø(ØØ(P Ú Q) Ú A)) ® (C ® Ø(ØØ(P Ú Q) Ú A))) replace proposition variable B by Ø(ØØ(P Ú Q) Ú A) in 64 107 ((ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø(ØØ(P Ú Q) Ú A))) replace proposition variable C by Ø(P Ú ØØ(Q Ú A)) in 106 108 ((D ® (Ø(P Ú ØØ(Q Ú A)) ® Ø(ØØ(P Ú Q) Ú A))) ® (((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® D) ® ((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø(ØØ(P Ú Q) Ú A))))) replace proposition variable C by (Ø(P Ú ØØ(Q Ú A)) ® Ø(ØØ(P Ú Q) Ú A)) in 101 109 (((ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø(ØØ(P Ú Q) Ú A))) ® (((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))) ® ((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø(ØØ(P Ú Q) Ú A))))) replace proposition variable D by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)) in 108 110 (((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))) ® ((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø(ØØ(P Ú Q) Ú A)))) modus ponens with 107, 109 111 ((Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø(ØØ(P Ú Q) Ú A))) modus ponens with 105, 110 112 (Ø(P Ú ØØ(Q Ú A)) ® Ø(ØØ(P Ú Q) Ú A)) modus ponens with 71, 111 113 (Ø(P Ú ØØ(Q Ú B)) ® Ø(ØØ(P Ú Q) Ú B)) replace proposition variable A by B in 112 114 (Ø(P Ú ØØ(C Ú B)) ® Ø(ØØ(P Ú C) Ú B)) replace proposition variable Q by C in 113 115 (Ø(D Ú ØØ(C Ú B)) ® Ø(ØØ(D Ú C) Ú B)) replace proposition variable P by D in 114 116 (Ø(D Ú ØØ(C Ú ØA)) ® Ø(ØØ(D Ú C) Ú ØA)) replace proposition variable B by ØA in 115 117 (Ø(D Ú ØØ(ØQ Ú ØA)) ® Ø(ØØ(D Ú ØQ) Ú ØA)) replace proposition variable C by ØQ in 116 118 (Ø(ØP Ú ØØ(ØQ Ú ØA)) ® Ø(ØØ(ØP Ú ØQ) Ú ØA)) replace proposition variable D by ØP in 117 119 ((P Ù Ø(ØQ Ú ØA)) ® Ø(ØØ(ØP Ú ØQ) Ú ØA)) reverse abbreviation and in 118 at occurence 1 120 ((P Ù (Q Ù A)) ® Ø(ØØ(ØP Ú ØQ) Ú ØA)) reverse abbreviation and in 119 at occurence 1 121 ((P Ù (Q Ù A)) ® (Ø(ØP Ú ØQ) Ù A)) reverse abbreviation and in 120 at occurence 1 122 ((P Ù (Q Ù A)) ® ((P Ù Q) Ù A)) reverse abbreviation and in 121 at occurence 1 qed

The conjunction is associative (second implication):

10. Proposition
(((P
Ù Q) Ù A) ® (P Ù (Q Ù A)))     (hilb27)

Proof:
 1 ((P Ú (Q Ú A)) ® ((P Ú Q) Ú A)) add proposition hilb14 2 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7 3 ((P ® A) ® (ØA ® ØP)) replace proposition variable Q by A in 2 4 ((B ® A) ® (ØA ® ØB)) replace proposition variable P by B in 3 5 ((B ® ((P Ú Q) Ú A)) ® (Ø((P Ú Q) Ú A) ® ØB)) replace proposition variable A by ((P Ú Q) Ú A) in 4 6 (((P Ú (Q Ú A)) ® ((P Ú Q) Ú A)) ® (Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A)))) replace proposition variable B by (P Ú (Q Ú A)) in 5 7 (Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) modus ponens with 1, 6 8 (P ® ØØP) add proposition hilb5 9 (A ® ØØA) replace proposition variable P by A in 8 10 ((P Ú Q) ® ØØ(P Ú Q)) replace proposition variable A by (P Ú Q) in 9 11 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 12 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 11 13 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 12 14 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 13 15 ((D ® C) ® ((A Ú D) ® (A Ú C))) replace proposition variable B by A in 14 16 ((D ® ØØ(P Ú Q)) ® ((A Ú D) ® (A Ú ØØ(P Ú Q)))) replace proposition variable C by ØØ(P Ú Q) in 15 17 (((P Ú Q) ® ØØ(P Ú Q)) ® ((A Ú (P Ú Q)) ® (A Ú ØØ(P Ú Q)))) replace proposition variable D by (P Ú Q) in 16 18 ((A Ú (P Ú Q)) ® (A Ú ØØ(P Ú Q))) modus ponens with 10, 17 19 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 20 ((P Ú B) ® (B Ú P)) replace proposition variable Q by B in 19 21 ((C Ú B) ® (B Ú C)) replace proposition variable P by C in 20 22 ((C Ú ØØ(P Ú Q)) ® (ØØ(P Ú Q) Ú C)) replace proposition variable B by ØØ(P Ú Q) in 21 23 ((A Ú ØØ(P Ú Q)) ® (ØØ(P Ú Q) Ú A)) replace proposition variable C by A in 22 24 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1 25 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 24 26 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 25 27 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 26 28 ((D ® C) ® (((A Ú (P Ú Q)) ® D) ® ((A Ú (P Ú Q)) ® C))) replace proposition variable B by (A Ú (P Ú Q)) in 27 29 ((D ® (ØØ(P Ú Q) Ú A)) ® (((A Ú (P Ú Q)) ® D) ® ((A Ú (P Ú Q)) ® (ØØ(P Ú Q) Ú A)))) replace proposition variable C by (ØØ(P Ú Q) Ú A) in 28 30 (((A Ú ØØ(P Ú Q)) ® (ØØ(P Ú Q) Ú A)) ® (((A Ú (P Ú Q)) ® (A Ú ØØ(P Ú Q))) ® ((A Ú (P Ú Q)) ® (ØØ(P Ú Q) Ú A)))) replace proposition variable D by (A Ú ØØ(P Ú Q)) in 29 31 (((A Ú (P Ú Q)) ® (A Ú ØØ(P Ú Q))) ® ((A Ú (P Ú Q)) ® (ØØ(P Ú Q) Ú A))) modus ponens with 23, 30 32 ((A Ú (P Ú Q)) ® (ØØ(P Ú Q) Ú A)) modus ponens with 18, 31 33 ((C Ú A) ® (A Ú C)) replace proposition variable B by A in 21 34 (((P Ú Q) Ú A) ® (A Ú (P Ú Q))) replace proposition variable C by (P Ú Q) in 33 35 ((D ® C) ® ((((P Ú Q) Ú A) ® D) ® (((P Ú Q) Ú A) ® C))) replace proposition variable B by ((P Ú Q) Ú A) in 27 36 ((D ® (ØØ(P Ú Q) Ú A)) ® ((((P Ú Q) Ú A) ® D) ® (((P Ú Q) Ú A) ® (ØØ(P Ú Q) Ú A)))) replace proposition variable C by (ØØ(P Ú Q) Ú A) in 35 37 (((A Ú (P Ú Q)) ® (ØØ(P Ú Q) Ú A)) ® ((((P Ú Q) Ú A) ® (A Ú (P Ú Q))) ® (((P Ú Q) Ú A) ® (ØØ(P Ú Q) Ú A)))) replace proposition variable D by (A Ú (P Ú Q)) in 36 38 ((((P Ú Q) Ú A) ® (A Ú (P Ú Q))) ® (((P Ú Q) Ú A) ® (ØØ(P Ú Q) Ú A))) modus ponens with 32, 37 39 (((P Ú Q) Ú A) ® (ØØ(P Ú Q) Ú A)) modus ponens with 34, 38 40 ((P ® B) ® (ØB ® ØP)) replace proposition variable Q by B in 2 41 ((C ® B) ® (ØB ® ØC)) replace proposition variable P by C in 40 42 ((C ® (ØØ(P Ú Q) Ú A)) ® (Ø(ØØ(P Ú Q) Ú A) ® ØC)) replace proposition variable B by (ØØ(P Ú Q) Ú A) in 41 43 ((((P Ú Q) Ú A) ® (ØØ(P Ú Q) Ú A)) ® (Ø(ØØ(P Ú Q) Ú A) ® Ø((P Ú Q) Ú A))) replace proposition variable C by ((P Ú Q) Ú A) in 42 44 (Ø(ØØ(P Ú Q) Ú A) ® Ø((P Ú Q) Ú A)) modus ponens with 39, 43 45 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1 46 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2 47 ((C ® Ø((P Ú Q) Ú A)) ® (ØØ((P Ú Q) Ú A) ® ØC)) replace proposition variable B by Ø((P Ú Q) Ú A) in 41 48 ((Ø(ØØ(P Ú Q) Ú A) ® Ø((P Ú Q) Ú A)) ® (ØØ((P Ú Q) Ú A) ® ØØ(ØØ(P Ú Q) Ú A))) replace proposition variable C by Ø(ØØ(P Ú Q) Ú A) in 47 49 (ØØ((P Ú Q) Ú A) ® ØØ(ØØ(P Ú Q) Ú A)) modus ponens with 44, 48 50 ((D ® C) ® ((Ø(P Ú (Q Ú A)) Ú D) ® (Ø(P Ú (Q Ú A)) Ú C))) replace proposition variable B by Ø(P Ú (Q Ú A)) in 14 51 ((D ® ØØ(ØØ(P Ú Q) Ú A)) ® ((Ø(P Ú (Q Ú A)) Ú D) ® (Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A)))) replace proposition variable C by ØØ(ØØ(P Ú Q) Ú A) in 50 52 ((ØØ((P Ú Q) Ú A) ® ØØ(ØØ(P Ú Q) Ú A)) ® ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) ® (Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A)))) replace proposition variable D by ØØ((P Ú Q) Ú A) in 51 53 ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) ® (Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A))) modus ponens with 49, 52 54 ((C Ú ØØ(ØØ(P Ú Q) Ú A)) ® (ØØ(ØØ(P Ú Q) Ú A) Ú C)) replace proposition variable B by ØØ(ØØ(P Ú Q) Ú A) in 21 55 ((Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A)) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) replace proposition variable C by Ø(P Ú (Q Ú A)) in 54 56 ((D ® C) ® (((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) ® D) ® ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) ® C))) replace proposition variable B by (Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) in 27 57 ((D ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) ® (((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) ® D) ® ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))))) replace proposition variable C by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 56 58 (((Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A)) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) ® (((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) ® (Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A))) ® ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))))) replace proposition variable D by (Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A)) in 57 59 (((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) ® (Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A))) ® ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))))) modus ponens with 55, 58 60 ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) modus ponens with 53, 59 61 ((C Ú Ø(P Ú (Q Ú A))) ® (Ø(P Ú (Q Ú A)) Ú C)) replace proposition variable B by Ø(P Ú (Q Ú A)) in 21 62 ((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® (Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A))) replace proposition variable C by ØØ((P Ú Q) Ú A) in 61 63 ((D ® C) ® (((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® D) ® ((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® C))) replace proposition variable B by (ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 27 64 ((D ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) ® (((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® D) ® ((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))))) replace proposition variable C by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 63 65 (((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) ® (((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® (Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A))) ® ((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))))) replace proposition variable D by (Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) in 64 66 (((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® (Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A))) ® ((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))))) modus ponens with 60, 65 67 ((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) modus ponens with 62, 66 68 ((P ® B) ® (ØP Ú B)) replace proposition variable Q by B in 45 69 ((C ® B) ® (ØC Ú B)) replace proposition variable P by C in 68 70 ((C ® Ø(P Ú (Q Ú A))) ® (ØC Ú Ø(P Ú (Q Ú A)))) replace proposition variable B by Ø(P Ú (Q Ú A)) in 69 71 ((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) replace proposition variable C by Ø((P Ú Q) Ú A) in 70 72 ((D ® C) ® (((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® D) ® ((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® C))) replace proposition variable B by (Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) in 27 73 ((D ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) ® (((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® D) ® ((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))))) replace proposition variable C by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 72 74 (((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) ® (((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) ® ((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))))) replace proposition variable D by (ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 73 75 (((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) ® ((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))))) modus ponens with 67, 74 76 ((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) modus ponens with 71, 75 77 ((ØP Ú B) ® (P ® B)) replace proposition variable Q by B in 46 78 ((ØC Ú B) ® (C ® B)) replace proposition variable P by C in 77 79 ((ØC Ú Ø(P Ú (Q Ú A))) ® (C ® Ø(P Ú (Q Ú A)))) replace proposition variable B by Ø(P Ú (Q Ú A)) in 78 80 ((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A)))) replace proposition variable C by Ø(ØØ(P Ú Q) Ú A) in 79 81 ((D ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A)))) ® (((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® D) ® ((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A)))))) replace proposition variable C by (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) in 72 82 (((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A)))) ® (((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) ® ((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A)))))) replace proposition variable D by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 81 83 (((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) ® ((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))))) modus ponens with 80, 82 84 ((Ø((P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A)))) modus ponens with 76, 83 85 (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) modus ponens with 7, 84 86 (ØØP ® P) add proposition hilb6 87 (ØØB ® B) replace proposition variable P by B in 86 88 (ØØ(Q Ú A) ® (Q Ú A)) replace proposition variable B by (Q Ú A) in 87 89 ((D ® C) ® ((P Ú D) ® (P Ú C))) replace proposition variable B by P in 14 90 ((D ® (Q Ú A)) ® ((P Ú D) ® (P Ú (Q Ú A)))) replace proposition variable C by (Q Ú A) in 89 91 ((ØØ(Q Ú A) ® (Q Ú A)) ® ((P Ú ØØ(Q Ú A)) ® (P Ú (Q Ú A)))) replace proposition variable D by ØØ(Q Ú A) in 90 92 ((P Ú ØØ(Q Ú A)) ® (P Ú (Q Ú A))) modus ponens with 88, 91 93 ((C ® (P Ú (Q Ú A))) ® (Ø(P Ú (Q Ú A)) ® ØC)) replace proposition variable B by (P Ú (Q Ú A)) in 41 94 (((P Ú ØØ(Q Ú A)) ® (P Ú (Q Ú A))) ® (Ø(P Ú (Q Ú A)) ® Ø(P Ú ØØ(Q Ú A)))) replace proposition variable C by (P Ú ØØ(Q Ú A)) in 93 95 (Ø(P Ú (Q Ú A)) ® Ø(P Ú ØØ(Q Ú A))) modus ponens with 92, 94 96 ((D ® C) ® ((ØØ(ØØ(P Ú Q) Ú A) Ú D) ® (ØØ(ØØ(P Ú Q) Ú A) Ú C))) replace proposition variable B by ØØ(ØØ(P Ú Q) Ú A) in 14 97 ((D ® Ø(P Ú ØØ(Q Ú A))) ® ((ØØ(ØØ(P Ú Q) Ú A) Ú D) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))))) replace proposition variable C by Ø(P Ú ØØ(Q Ú A)) in 96 98 ((Ø(P Ú (Q Ú A)) ® Ø(P Ú ØØ(Q Ú A))) ® ((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))))) replace proposition variable D by Ø(P Ú (Q Ú A)) in 97 99 ((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))) modus ponens with 95, 98 100 ((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) replace proposition variable C by Ø(ØØ(P Ú Q) Ú A) in 70 101 ((D ® C) ® (((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® D) ® ((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® C))) replace proposition variable B by (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) in 27 102 ((D ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))) ® (((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® D) ® ((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))))) replace proposition variable C by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))) in 101 103 (((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))) ® (((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) ® ((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))))) replace proposition variable D by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 102 104 (((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) ® ((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))))) modus ponens with 99, 103 105 ((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))) modus ponens with 100, 104 106 ((ØC Ú Ø(P Ú ØØ(Q Ú A))) ® (C ® Ø(P Ú ØØ(Q Ú A)))) replace proposition variable B by Ø(P Ú ØØ(Q Ú A)) in 78 107 ((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))) ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú ØØ(Q Ú A)))) replace proposition variable C by Ø(ØØ(P Ú Q) Ú A) in 106 108 ((D ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú ØØ(Q Ú A)))) ® (((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® D) ® ((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú ØØ(Q Ú A)))))) replace proposition variable C by (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú ØØ(Q Ú A))) in 101 109 (((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))) ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú ØØ(Q Ú A)))) ® (((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))) ® ((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú ØØ(Q Ú A)))))) replace proposition variable D by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))) in 108 110 (((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))) ® ((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú ØØ(Q Ú A))))) modus ponens with 107, 109 111 ((Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú (Q Ú A))) ® (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú ØØ(Q Ú A)))) modus ponens with 105, 110 112 (Ø(ØØ(P Ú Q) Ú A) ® Ø(P Ú ØØ(Q Ú A))) modus ponens with 85, 111 113 (Ø(ØØ(P Ú Q) Ú B) ® Ø(P Ú ØØ(Q Ú B))) replace proposition variable A by B in 112 114 (Ø(ØØ(P Ú C) Ú B) ® Ø(P Ú ØØ(C Ú B))) replace proposition variable Q by C in 113 115 (Ø(ØØ(D Ú C) Ú B) ® Ø(D Ú ØØ(C Ú B))) replace proposition variable P by D in 114 116 (Ø(ØØ(D Ú C) Ú ØA) ® Ø(D Ú ØØ(C Ú ØA))) replace proposition variable B by ØA in 115 117 (Ø(ØØ(D Ú ØQ) Ú ØA) ® Ø(D Ú ØØ(ØQ Ú ØA))) replace proposition variable C by ØQ in 116 118 (Ø(ØØ(ØP Ú ØQ) Ú ØA) ® Ø(ØP Ú ØØ(ØQ Ú ØA))) replace proposition variable D by ØP in 117 119 ((Ø(ØP Ú ØQ) Ù A) ® Ø(ØP Ú ØØ(ØQ Ú ØA))) reverse abbreviation and in 118 at occurence 1 120 (((P Ù Q) Ù A) ® Ø(ØP Ú ØØ(ØQ Ú ØA))) reverse abbreviation and in 119 at occurence 1 121 (((P Ù Q) Ù A) ® (P Ù Ø(ØQ Ú ØA))) reverse abbreviation and in 120 at occurence 1 122 (((P Ù Q) Ù A) ® (P Ù (Q Ù A))) reverse abbreviation and in 121 at occurence 1 qed

Form for the conjunction rule:

11. Proposition
(P
® (Q ® (P Ù Q)))     (hilb28)

Proof:
 1 (P Ú ØP) add proposition hilb4 2 ((ØP Ú ØQ) Ú Ø(ØP Ú ØQ)) replace proposition variable P by (ØP Ú ØQ) in 1 3 (((P Ú Q) Ú A) ® (P Ú (Q Ú A))) add proposition hilb15 4 (((P Ú Q) Ú B) ® (P Ú (Q Ú B))) replace proposition variable A by B in 3 5 (((P Ú C) Ú B) ® (P Ú (C Ú B))) replace proposition variable Q by C in 4 6 (((D Ú C) Ú B) ® (D Ú (C Ú B))) replace proposition variable P by D in 5 7 (((D Ú C) Ú Ø(ØP Ú ØQ)) ® (D Ú (C Ú Ø(ØP Ú ØQ)))) replace proposition variable B by Ø(ØP Ú ØQ) in 6 8 (((D Ú ØQ) Ú Ø(ØP Ú ØQ)) ® (D Ú (ØQ Ú Ø(ØP Ú ØQ)))) replace proposition variable C by ØQ in 7 9 (((ØP Ú ØQ) Ú Ø(ØP Ú ØQ)) ® (ØP Ú (ØQ Ú Ø(ØP Ú ØQ)))) replace proposition variable D by ØP in 8 10 (ØP Ú (ØQ Ú Ø(ØP Ú ØQ))) modus ponens with 2, 9 11 (P ® (ØQ Ú Ø(ØP Ú ØQ))) reverse abbreviation impl in 10 at occurence 1 12 (P ® (Q ® Ø(ØP Ú ØQ))) reverse abbreviation impl in 11 at occurence 1 13 (P ® (Q ® (P Ù Q))) reverse abbreviation and in 12 at occurence 1 qed

Preconditions could be put together in a conjunction (first direction):

12. Proposition
((P
® (Q ® A)) ® ((P Ù Q) ® A))     (hilb29)

Proof:
 1 (P ® P) add proposition hilb2 2 (Q ® Q) replace proposition variable P by Q in 1 3 ((P ® (Q ® A)) ® (P ® (Q ® A))) replace proposition variable Q by (P ® (Q ® A)) in 2 4 ((P ® (Q ® A)) ® (ØP Ú (Q ® A))) use abbreviation impl in 3 at occurence 4 5 ((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) use abbreviation impl in 4 at occurence 4 6 ((P Ú (Q Ú A)) ® ((P Ú Q) Ú A)) add proposition hilb14 7 ((P Ú (Q Ú B)) ® ((P Ú Q) Ú B)) replace proposition variable A by B in 6 8 ((P Ú (C Ú B)) ® ((P Ú C) Ú B)) replace proposition variable Q by C in 7 9 ((D Ú (C Ú B)) ® ((D Ú C) Ú B)) replace proposition variable P by D in 8 10 ((D Ú (C Ú A)) ® ((D Ú C) Ú A)) replace proposition variable B by A in 9 11 ((D Ú (ØQ Ú A)) ® ((D Ú ØQ) Ú A)) replace proposition variable C by ØQ in 10 12 ((ØP Ú (ØQ Ú A)) ® ((ØP Ú ØQ) Ú A)) replace proposition variable D by ØP in 11 13 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1 14 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2 15 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 16 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 15 17 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 16 18 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 17 19 ((D ® C) ® ((Ø(P ® (Q ® A)) Ú D) ® (Ø(P ® (Q ® A)) Ú C))) replace proposition variable B by Ø(P ® (Q ® A)) in 18 20 ((D ® ((ØP Ú ØQ) Ú A)) ® ((Ø(P ® (Q ® A)) Ú D) ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A)))) replace proposition variable C by ((ØP Ú ØQ) Ú A) in 19 21 (((ØP Ú (ØQ Ú A)) ® ((ØP Ú ØQ) Ú A)) ® ((Ø(P ® (Q ® A)) Ú (ØP Ú (ØQ Ú A))) ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A)))) replace proposition variable D by (ØP Ú (ØQ Ú A)) in 20 22 ((Ø(P ® (Q ® A)) Ú (ØP Ú (ØQ Ú A))) ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A))) modus ponens with 12, 21 23 ((P ® B) ® (ØP Ú B)) replace proposition variable Q by B in 13 24 ((C ® B) ® (ØC Ú B)) replace proposition variable P by C in 23 25 ((C ® (ØP Ú (ØQ Ú A))) ® (ØC Ú (ØP Ú (ØQ Ú A)))) replace proposition variable B by (ØP Ú (ØQ Ú A)) in 24 26 (((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® (Ø(P ® (Q ® A)) Ú (ØP Ú (ØQ Ú A)))) replace proposition variable C by (P ® (Q ® A)) in 25 27 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1 28 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 27 29 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 28 30 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 29 31 ((D ® C) ® ((((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® D) ® (((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® C))) replace proposition variable B by ((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) in 30 32 ((D ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A))) ® ((((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® D) ® (((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A))))) replace proposition variable C by (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A)) in 31 33 (((Ø(P ® (Q ® A)) Ú (ØP Ú (ØQ Ú A))) ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A))) ® ((((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® (Ø(P ® (Q ® A)) Ú (ØP Ú (ØQ Ú A)))) ® (((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A))))) replace proposition variable D by (Ø(P ® (Q ® A)) Ú (ØP Ú (ØQ Ú A))) in 32 34 ((((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® (Ø(P ® (Q ® A)) Ú (ØP Ú (ØQ Ú A)))) ® (((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A)))) modus ponens with 22, 33 35 (((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A))) modus ponens with 26, 34 36 ((ØP Ú B) ® (P ® B)) replace proposition variable Q by B in 14 37 ((ØC Ú B) ® (C ® B)) replace proposition variable P by C in 36 38 ((ØC Ú ((ØP Ú ØQ) Ú A)) ® (C ® ((ØP Ú ØQ) Ú A))) replace proposition variable B by ((ØP Ú ØQ) Ú A) in 37 39 ((Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A)) ® ((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A))) replace proposition variable C by (P ® (Q ® A)) in 38 40 ((D ® ((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A))) ® ((((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® D) ® (((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® ((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A))))) replace proposition variable C by ((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) in 31 41 (((Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A)) ® ((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A))) ® ((((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A))) ® (((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® ((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A))))) replace proposition variable D by (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A)) in 40 42 ((((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A))) ® (((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® ((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)))) modus ponens with 39, 41 43 (((P ® (Q ® A)) ® (ØP Ú (ØQ Ú A))) ® ((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A))) modus ponens with 35, 42 44 ((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) modus ponens with 5, 43 45 (P ® ØØP) add proposition hilb5 46 (A ® ØØA) replace proposition variable P by A in 45 47 ((ØP Ú ØQ) ® ØØ(ØP Ú ØQ)) replace proposition variable A by (ØP Ú ØQ) in 46 48 ((D ® C) ® ((A Ú D) ® (A Ú C))) replace proposition variable B by A in 18 49 ((D ® ØØ(ØP Ú ØQ)) ® ((A Ú D) ® (A Ú ØØ(ØP Ú ØQ)))) replace proposition variable C by ØØ(ØP Ú ØQ) in 48 50 (((ØP Ú ØQ) ® ØØ(ØP Ú ØQ)) ® ((A Ú (ØP Ú ØQ)) ® (A Ú ØØ(ØP Ú ØQ)))) replace proposition variable D by (ØP Ú ØQ) in 49 51 ((A Ú (ØP Ú ØQ)) ® (A Ú ØØ(ØP Ú ØQ))) modus ponens with 47, 50 52 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 53 ((P Ú B) ® (B Ú P)) replace proposition variable Q by B in 52 54 ((C Ú B) ® (B Ú C)) replace proposition variable P by C in 53 55 ((C Ú ØØ(ØP Ú ØQ)) ® (ØØ(ØP Ú ØQ) Ú C)) replace proposition variable B by ØØ(ØP Ú ØQ) in 54 56 ((A Ú ØØ(ØP Ú ØQ)) ® (ØØ(ØP Ú ØQ) Ú A)) replace proposition variable C by A in 55 57 ((D ® C) ® (((A Ú (ØP Ú ØQ)) ® D) ® ((A Ú (ØP Ú ØQ)) ® C))) replace proposition variable B by (A Ú (ØP Ú ØQ)) in 30 58 ((D ® (ØØ(ØP Ú ØQ) Ú A)) ® (((A Ú (ØP Ú ØQ)) ® D) ® ((A Ú (ØP Ú ØQ)) ® (ØØ(ØP Ú ØQ) Ú A)))) replace proposition variable C by (ØØ(ØP Ú ØQ) Ú A) in 57 59 (((A Ú ØØ(ØP Ú ØQ)) ® (ØØ(ØP Ú ØQ) Ú A)) ® (((A Ú (ØP Ú ØQ)) ® (A Ú ØØ(ØP Ú ØQ))) ® ((A Ú (ØP Ú ØQ)) ® (ØØ(ØP Ú ØQ) Ú A)))) replace proposition variable D by (A Ú ØØ(ØP Ú ØQ)) in 58 60 (((A Ú (ØP Ú ØQ)) ® (A Ú ØØ(ØP Ú ØQ))) ® ((A Ú (ØP Ú ØQ)) ® (ØØ(ØP Ú ØQ) Ú A))) modus ponens with 56, 59 61 ((A Ú (ØP Ú ØQ)) ® (ØØ(ØP Ú ØQ) Ú A)) modus ponens with 51, 60 62 ((C Ú A) ® (A Ú C)) replace proposition variable B by A in 54 63 (((ØP Ú ØQ) Ú A) ® (A Ú (ØP Ú ØQ))) replace proposition variable C by (ØP Ú ØQ) in 62 64 ((D ® C) ® ((((ØP Ú ØQ) Ú A) ® D) ® (((ØP Ú ØQ) Ú A) ® C))) replace proposition variable B by ((ØP Ú ØQ) Ú A) in 30 65 ((D ® (ØØ(ØP Ú ØQ) Ú A)) ® ((((ØP Ú ØQ) Ú A) ® D) ® (((ØP Ú ØQ) Ú A) ® (ØØ(ØP Ú ØQ) Ú A)))) replace proposition variable C by (ØØ(ØP Ú ØQ) Ú A) in 64 66 (((A Ú (ØP Ú ØQ)) ® (ØØ(ØP Ú ØQ) Ú A)) ® ((((ØP Ú ØQ) Ú A) ® (A Ú (ØP Ú ØQ))) ® (((ØP Ú ØQ) Ú A) ® (ØØ(ØP Ú ØQ) Ú A)))) replace proposition variable D by (A Ú (ØP Ú ØQ)) in 65 67 ((((ØP Ú ØQ) Ú A) ® (A Ú (ØP Ú ØQ))) ® (((ØP Ú ØQ) Ú A) ® (ØØ(ØP Ú ØQ) Ú A))) modus ponens with 61, 66 68 (((ØP Ú ØQ) Ú A) ® (ØØ(ØP Ú ØQ) Ú A)) modus ponens with 63, 67 69 ((D ® (ØØ(ØP Ú ØQ) Ú A)) ® ((Ø(P ® (Q ® A)) Ú D) ® (Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A)))) replace proposition variable C by (ØØ(ØP Ú ØQ) Ú A) in 19 70 ((((ØP Ú ØQ) Ú A) ® (ØØ(ØP Ú ØQ) Ú A)) ® ((Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A)) ® (Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A)))) replace proposition variable D by ((ØP Ú ØQ) Ú A) in 69 71 ((Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A)) ® (Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A))) modus ponens with 68, 70 72 ((C ® ((ØP Ú ØQ) Ú A)) ® (ØC Ú ((ØP Ú ØQ) Ú A))) replace proposition variable B by ((ØP Ú ØQ) Ú A) in 24 73 (((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A))) replace proposition variable C by (P ® (Q ® A)) in 72 74 ((D ® C) ® ((((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® D) ® (((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® C))) replace proposition variable B by ((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) in 30 75 ((D ® (Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A))) ® ((((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® D) ® (((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® (Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A))))) replace proposition variable C by (Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A)) in 74 76 (((Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A)) ® (Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A))) ® ((((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A))) ® (((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® (Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A))))) replace proposition variable D by (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A)) in 75 77 ((((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® (Ø(P ® (Q ® A)) Ú ((ØP Ú ØQ) Ú A))) ® (((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® (Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A)))) modus ponens with 71, 76 78 (((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® (Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A))) modus ponens with 73, 77 79 ((ØC Ú (ØØ(ØP Ú ØQ) Ú A)) ® (C ® (ØØ(ØP Ú ØQ) Ú A))) replace proposition variable B by (ØØ(ØP Ú ØQ) Ú A) in 37 80 ((Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A)) ® ((P ® (Q ® A)) ® (ØØ(ØP Ú ØQ) Ú A))) replace proposition variable C by (P ® (Q ® A)) in 79 81 ((D ® ((P ® (Q ® A)) ® (ØØ(ØP Ú ØQ) Ú A))) ® ((((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® D) ® (((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® ((P ® (Q ® A)) ® (ØØ(ØP Ú ØQ) Ú A))))) replace proposition variable C by ((P ® (Q ® A)) ® (ØØ(ØP Ú ØQ) Ú A)) in 74 82 (((Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A)) ® ((P ® (Q ® A)) ® (ØØ(ØP Ú ØQ) Ú A))) ® ((((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® (Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A))) ® (((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® ((P ® (Q ® A)) ® (ØØ(ØP Ú ØQ) Ú A))))) replace proposition variable D by (Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A)) in 81 83 ((((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® (Ø(P ® (Q ® A)) Ú (ØØ(ØP Ú ØQ) Ú A))) ® (((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® ((P ® (Q ® A)) ® (ØØ(ØP Ú ØQ) Ú A)))) modus ponens with 80, 82 84 (((P ® (Q ® A)) ® ((ØP Ú ØQ) Ú A)) ® ((P ® (Q ® A)) ® (ØØ(ØP Ú ØQ) Ú A))) modus ponens with 78, 83 85 ((P ® (Q ® A)) ® (ØØ(ØP Ú ØQ) Ú A)) modus ponens with 44, 84 86 ((P ® (Q ® A)) ® (Ø(ØP Ú ØQ) ® A)) reverse abbreviation impl in 85 at occurence 1 87 ((P ® (Q ® A)) ® ((P Ù Q) ® A)) reverse abbreviation and in 86 at occurence 1 qed

Preconditions could be put together in a conjunction (second direction):

13. Proposition
(((P
Ù Q) ® A) ® (P ® (Q ® A)))     (hilb30)

Proof:
 1 (P ® P) add proposition hilb2 2 (Q ® Q) replace proposition variable P by Q in 1 3 ((P ® (Q ® A)) ® (P ® (Q ® A))) replace proposition variable Q by (P ® (Q ® A)) in 2 4 ((ØP Ú (Q ® A)) ® (P ® (Q ® A))) use abbreviation impl in 3 at occurence 2 5 ((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) use abbreviation impl in 4 at occurence 2 6 (((P Ú Q) Ú A) ® (P Ú (Q Ú A))) add proposition hilb15 7 (((P Ú Q) Ú B) ® (P Ú (Q Ú B))) replace proposition variable A by B in 6 8 (((P Ú C) Ú B) ® (P Ú (C Ú B))) replace proposition variable Q by C in 7 9 (((D Ú C) Ú B) ® (D Ú (C Ú B))) replace proposition variable P by D in 8 10 (((D Ú C) Ú A) ® (D Ú (C Ú A))) replace proposition variable B by A in 9 11 (((D Ú ØQ) Ú A) ® (D Ú (ØQ Ú A))) replace proposition variable C by ØQ in 10 12 (((ØP Ú ØQ) Ú A) ® (ØP Ú (ØQ Ú A))) replace proposition variable D by ØP in 11 13 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1 14 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2 15 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7 16 ((P ® B) ® (ØB ® ØP)) replace proposition variable Q by B in 15 17 ((C ® B) ® (ØB ® ØC)) replace proposition variable P by C in 16 18 ((C ® (ØP Ú (ØQ Ú A))) ® (Ø(ØP Ú (ØQ Ú A)) ® ØC)) replace proposition variable B by (ØP Ú (ØQ Ú A)) in 17 19 ((((ØP Ú ØQ) Ú A) ® (ØP Ú (ØQ Ú A))) ® (Ø(ØP Ú (ØQ Ú A)) ® Ø((ØP Ú ØQ) Ú A))) replace proposition variable C by ((ØP Ú ØQ) Ú A) in 18 20 (Ø(ØP Ú (ØQ Ú A)) ® Ø((ØP Ú ØQ) Ú A)) modus ponens with 12, 19 21 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 22 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 21 23 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 22 24 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 23 25 ((D ® C) ® (((P ® (Q ® A)) Ú D) ® ((P ® (Q ® A)) Ú C))) replace proposition variable B by (P ® (Q ® A)) in 24 26 ((D ® Ø((ØP Ú ØQ) Ú A)) ® (((P ® (Q ® A)) Ú D) ® ((P ® (Q ® A)) Ú Ø((ØP Ú ØQ) Ú A)))) replace proposition variable C by Ø((ØP Ú ØQ) Ú A) in 25 27 ((Ø(ØP Ú (ØQ Ú A)) ® Ø((ØP Ú ØQ) Ú A)) ® (((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) ® ((P ® (Q ® A)) Ú Ø((ØP Ú ØQ) Ú A)))) replace proposition variable D by Ø(ØP Ú (ØQ Ú A)) in 26 28 (((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) ® ((P ® (Q ® A)) Ú Ø((ØP Ú ØQ) Ú A))) modus ponens with 20, 27 29 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 30 ((P Ú B) ® (B Ú P)) replace proposition variable Q by B in 29 31 ((C Ú B) ® (B Ú C)) replace proposition variable P by C in 30 32 ((C Ú Ø((ØP Ú ØQ) Ú A)) ® (Ø((ØP Ú ØQ) Ú A) Ú C)) replace proposition variable B by Ø((ØP Ú ØQ) Ú A) in 31 33 (((P ® (Q ® A)) Ú Ø((ØP Ú ØQ) Ú A)) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) replace proposition variable C by (P ® (Q ® A)) in 32 34 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1 35 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 34 36 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 35 37 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 36 38 ((D ® C) ® ((((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) ® D) ® (((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) ® C))) replace proposition variable B by ((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) in 37 39 ((D ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) ® ((((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) ® D) ® (((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))))) replace proposition variable C by (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A))) in 38 40 ((((P ® (Q ® A)) Ú Ø((ØP Ú ØQ) Ú A)) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) ® ((((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) ® ((P ® (Q ® A)) Ú Ø((ØP Ú ØQ) Ú A))) ® (((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))))) replace proposition variable D by ((P ® (Q ® A)) Ú Ø((ØP Ú ØQ) Ú A)) in 39 41 ((((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) ® ((P ® (Q ® A)) Ú Ø((ØP Ú ØQ) Ú A))) ® (((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A))))) modus ponens with 33, 40 42 (((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) modus ponens with 28, 41 43 ((C Ú (P ® (Q ® A))) ® ((P ® (Q ® A)) Ú C)) replace proposition variable B by (P ® (Q ® A)) in 31 44 ((Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A))) ® ((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A)))) replace proposition variable C by Ø(ØP Ú (ØQ Ú A)) in 43 45 ((D ® C) ® (((Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A))) ® D) ® ((Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A))) ® C))) replace proposition variable B by (Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A))) in 37 46 ((D ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) ® (((Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A))) ® D) ® ((Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))))) replace proposition variable C by (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A))) in 45 47 ((((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) ® (((Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A))) ® ((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A)))) ® ((Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))))) replace proposition variable D by ((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A))) in 46 48 (((Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A))) ® ((P ® (Q ® A)) Ú Ø(ØP Ú (ØQ Ú A)))) ® ((Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A))))) modus ponens with 42, 47 49 ((Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) modus ponens with 44, 48 50 ((P ® B) ® (ØP Ú B)) replace proposition variable Q by B in 13 51 ((C ® B) ® (ØC Ú B)) replace proposition variable P by C in 50 52 ((C ® (P ® (Q ® A))) ® (ØC Ú (P ® (Q ® A)))) replace proposition variable B by (P ® (Q ® A)) in 51 53 (((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® (Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A)))) replace proposition variable C by (ØP Ú (ØQ Ú A)) in 52 54 ((D ® C) ® ((((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® D) ® (((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® C))) replace proposition variable B by ((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) in 37 55 ((D ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) ® ((((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® D) ® (((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))))) replace proposition variable C by (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A))) in 54 56 (((Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) ® ((((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® (Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A)))) ® (((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))))) replace proposition variable D by (Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A))) in 55 57 ((((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® (Ø(ØP Ú (ØQ Ú A)) Ú (P ® (Q ® A)))) ® (((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A))))) modus ponens with 49, 56 58 (((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) modus ponens with 53, 57 59 ((ØP Ú B) ® (P ® B)) replace proposition variable Q by B in 14 60 ((ØC Ú B) ® (C ® B)) replace proposition variable P by C in 59 61 ((ØC Ú (P ® (Q ® A))) ® (C ® (P ® (Q ® A)))) replace proposition variable B by (P ® (Q ® A)) in 60 62 ((Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A))) ® (((ØP Ú ØQ) Ú A) ® (P ® (Q ® A)))) replace proposition variable C by ((ØP Ú ØQ) Ú A) in 61 63 ((D ® (((ØP Ú ØQ) Ú A) ® (P ® (Q ® A)))) ® ((((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® D) ® (((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® (((ØP Ú ØQ) Ú A) ® (P ® (Q ® A)))))) replace proposition variable C by (((ØP Ú ØQ) Ú A) ® (P ® (Q ® A))) in 54 64 (((Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A))) ® (((ØP Ú ØQ) Ú A) ® (P ® (Q ® A)))) ® ((((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) ® (((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® (((ØP Ú ØQ) Ú A) ® (P ® (Q ® A)))))) replace proposition variable D by (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A))) in 63 65 ((((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ®