for questions or link request: module admin

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 ® (Q ® A)))) ® (((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® (((ØP Ú ØQ) Ú A) ® (P ® (Q ® A))))) modus ponens with 62, 64
66 (((ØP Ú (ØQ Ú A)) ® (P ® (Q ® A))) ® (((ØP Ú ØQ) Ú A) ® (P ® (Q ® A)))) modus ponens with 58, 65
67 (((ØP Ú ØQ) Ú A) ® (P ® (Q ® A))) modus ponens with 5, 66
68 (ØØP ® P) add proposition hilb6
69 (ØØA ® A) replace proposition variable P by A in 68
70 (ØØ(ØP Ú ØQ) ® (ØP Ú ØQ)) replace proposition variable A by (ØP Ú ØQ) in 69
71 ((D ® C) ® ((A Ú D) ® (A Ú C))) replace proposition variable B by A in 24
72 ((D ® (ØP Ú ØQ)) ® ((A Ú D) ® (A Ú (ØP Ú ØQ)))) replace proposition variable C by (ØP Ú ØQ) in 71
73 ((ØØ(ØP Ú ØQ) ® (ØP Ú ØQ)) ® ((A Ú ØØ(ØP Ú ØQ)) ® (A Ú (ØP Ú ØQ)))) replace proposition variable D by ØØ(ØP Ú ØQ) in 72
74 ((A Ú ØØ(ØP Ú ØQ)) ® (A Ú (ØP Ú ØQ))) modus ponens with 70, 73
75 ((C Ú (ØP Ú ØQ)) ® ((ØP Ú ØQ) Ú C)) replace proposition variable B by (ØP Ú ØQ) in 31
76 ((A Ú (ØP Ú ØQ)) ® ((ØP Ú ØQ) Ú A)) replace proposition variable C by A in 75
77 ((D ® C) ® (((A Ú ØØ(ØP Ú ØQ)) ® D) ® ((A Ú ØØ(ØP Ú ØQ)) ® C))) replace proposition variable B by (A Ú ØØ(ØP Ú ØQ)) in 37
78 ((D ® ((ØP Ú ØQ) Ú A)) ® (((A Ú ØØ(ØP Ú ØQ)) ® D) ® ((A Ú ØØ(ØP Ú ØQ)) ® ((ØP Ú ØQ) Ú A)))) replace proposition variable C by ((ØP Ú ØQ) Ú A) in 77
79 (((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 78
80 (((A Ú ØØ(ØP Ú ØQ)) ® (A Ú (ØP Ú ØQ))) ® ((A Ú ØØ(ØP Ú ØQ)) ® ((ØP Ú ØQ) Ú A))) modus ponens with 76, 79
81 ((A Ú ØØ(ØP Ú ØQ)) ® ((ØP Ú ØQ) Ú A)) modus ponens with 74, 80
82 ((C Ú A) ® (A Ú C)) replace proposition variable B by A in 31
83 ((ØØ(ØP Ú ØQ) Ú A) ® (A Ú ØØ(ØP Ú ØQ))) replace proposition variable C by ØØ(ØP Ú ØQ) in 82
84 ((D ® C) ® (((ØØ(ØP Ú ØQ) Ú A) ® D) ® ((ØØ(ØP Ú ØQ) Ú A) ® C))) replace proposition variable B by (ØØ(ØP Ú ØQ) Ú A) in 37
85 ((D ® ((ØP Ú ØQ) Ú A)) ® (((ØØ(ØP Ú ØQ) Ú A) ® D) ® ((ØØ(ØP Ú ØQ) Ú A) ® ((ØP Ú ØQ) Ú A)))) replace proposition variable C by ((ØP Ú ØQ) Ú A) in 84
86 (((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 85
87 (((ØØ(ØP Ú ØQ) Ú A) ® (A Ú ØØ(ØP Ú ØQ))) ® ((ØØ(ØP Ú ØQ) Ú A) ® ((ØP Ú ØQ) Ú A))) modus ponens with 81, 86
88 ((ØØ(ØP Ú ØQ) Ú A) ® ((ØP Ú ØQ) Ú A)) modus ponens with 83, 87
89 ((C ® ((ØP Ú ØQ) Ú A)) ® (Ø((ØP Ú ØQ) Ú A) ® ØC)) replace proposition variable B by ((ØP Ú ØQ) Ú A) in 17
90 (((ØØ(ØP Ú ØQ) Ú A) ® ((ØP Ú ØQ) Ú A)) ® (Ø((ØP Ú ØQ) Ú A) ® Ø(ØØ(ØP Ú ØQ) Ú A))) replace proposition variable C by (ØØ(ØP Ú ØQ) Ú A) in 89
91 (Ø((ØP Ú ØQ) Ú A) ® Ø(ØØ(ØP Ú ØQ) Ú A)) modus ponens with 88, 90
92 ((D ® Ø(ØØ(ØP Ú ØQ) Ú A)) ® (((P ® (Q ® A)) Ú D) ® ((P ® (Q ® A)) Ú Ø(ØØ(ØP Ú ØQ) Ú A)))) replace proposition variable C by Ø(ØØ(ØP Ú ØQ) Ú A) in 25
93 ((Ø((Ø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 92
94 (((P ® (Q ® A)) Ú Ø((ØP Ú ØQ) Ú A)) ® ((P ® (Q ® A)) Ú Ø(ØØ(ØP Ú ØQ) Ú A))) modus ponens with 91, 93
95 ((C Ú Ø(ØØ(ØP Ú ØQ) Ú A)) ® (Ø(ØØ(ØP Ú ØQ) Ú A) Ú C)) replace proposition variable B by Ø(ØØ(ØP Ú ØQ) Ú A) in 31
96 (((P ® (Q ® A)) Ú Ø(ØØ(ØP Ú ØQ) Ú A)) ® (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) replace proposition variable C by (P ® (Q ® A)) in 95
97 ((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
98 ((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 97
99 ((((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 98
100 ((((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 96, 99
101 (((P ® (Q ® A)) Ú Ø((ØP Ú ØQ) Ú A)) ® (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) modus ponens with 94, 100
102 ((Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A))) ® ((P ® (Q ® A)) Ú Ø((ØP Ú ØQ) Ú A))) replace proposition variable C by Ø((ØP Ú ØQ) Ú A) in 43
103 ((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
104 ((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 103
105 ((((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 104
106 (((Ø((Ø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 101, 105
107 ((Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A))) ® (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) modus ponens with 102, 106
108 ((((ØP Ú ØQ) Ú A) ® (P ® (Q ® A))) ® (Ø((ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) replace proposition variable C by ((ØP Ú ØQ) Ú A) in 52
109 ((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
110 ((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 109
111 (((Ø((Ø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 110
112 (((((Ø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, 111
113 ((((ØP Ú ØQ) Ú A) ® (P ® (Q ® A))) ® (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P ® (Q ® A)))) modus ponens with 108, 112
114 ((Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P ® (Q ® A))) ® ((ØØ(ØP Ú ØQ) Ú A) ® (P ® (Q ® A)))) replace proposition variable C by (ØØ(ØP Ú ØQ) Ú A) in 61
115 ((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 109
116 (((Ø(ØØ(Ø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 115
117 (((((Ø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 114, 116
118 ((((ØP Ú ØQ) Ú A) ® (P ® (Q ® A))) ® ((ØØ(ØP Ú ØQ) Ú A) ® (P ® (Q ® A)))) modus ponens with 113, 117
119 ((ØØ(ØP Ú ØQ) Ú A) ® (P ® (Q ® A))) modus ponens with 67, 118
120 ((Ø(ØP Ú ØQ) ® A) ® (P ® (Q ® A))) reverse abbreviation impl in 119 at occurence 1
121 (((P Ù Q) ® A) ® (P ® (Q ® A))) reverse abbreviation and in 120 at occurence 1
qed

Absorbtion of a conjunction (first direction):

14. Proposition
      ((P Ù P) ® P)     (hilb31)

Proof:
1 ((P Ù Q) ® P) add proposition hilb24
2 ((P Ù P) ® P) replace proposition variable Q by P in 1
qed

Absorbtion of a conjunction (second direction):

15. Proposition
      (P ® (P Ù P))     (hilb32)

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

Absorbtion of identical preconditions (first direction):

16. Proposition
      ((P ® (P ® Q)) ® (P ® Q))     (hilb33)

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

Absorbtion of identical preconditions (second direction):

17. Proposition
      ((P ® Q) ® (P ® (P ® Q)))     (hilb34)

Proof:
1 (((P Ù Q) ® A) ® (P ® (Q ® A))) add proposition hilb30
2 (((P Ù Q) ® B) ® (P ® (Q ® B))) replace proposition variable A by B in 1
3 (((P Ù C) ® B) ® (P ® (C ® B))) replace proposition variable Q by C in 2
4 (((D Ù C) ® B) ® (D ® (C ® B))) replace proposition variable P by D in 3
5 (((D Ù C) ® Q) ® (D ® (C ® Q))) replace proposition variable B by Q in 4
6 (((D Ù P) ® Q) ® (D ® (P ® Q))) replace proposition variable C by P in 5
7 (((P Ù P) ® Q) ® (P ® (P ® Q))) replace proposition variable D by P in 6
8 ((P Ù P) ® P) add proposition hilb31
9 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1
10 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2
11 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7
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 (((P Ù P) ® P) ® (ØP ® Ø(P Ù P))) replace proposition variable B by (P Ù P) in 14
16 (ØP ® Ø(P Ù P)) modus ponens with 8, 15
17 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4
18 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 17
19 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 18
20 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 19
21 ((D ® C) ® ((Q Ú D) ® (Q Ú C))) replace proposition variable B by Q in 20
22 ((D ® Ø(P Ù P)) ® ((Q Ú D) ® (Q Ú Ø(P Ù P)))) replace proposition variable C by Ø(P Ù P) in 21
23 ((ØP ® Ø(P Ù P)) ® ((Q Ú ØP) ® (Q Ú Ø(P Ù P)))) replace proposition variable D by ØP in 22
24 ((Q Ú ØP) ® (Q Ú Ø(P Ù P))) modus ponens with 16, 23
25 ((P Ú Q) ® (Q Ú P)) add axiom axiom3
26 ((P Ú A) ® (A Ú P)) replace proposition variable Q by A in 25
27 ((B Ú A) ® (A Ú B)) replace proposition variable P by B in 26
28 ((B Ú Ø(P Ù P)) ® (Ø(P Ù P) Ú B)) replace proposition variable A by Ø(P Ù P) in 27
29 ((Q Ú Ø(P Ù P)) ® (Ø(P Ù P) Ú Q)) replace proposition variable B by 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) ® (((Q Ú ØP) ® D) ® ((Q Ú ØP) ® C))) replace proposition variable B by (Q Ú ØP) in 33
35 ((D ® (Ø(P Ù P) Ú Q)) ® (((Q Ú ØP) ® D) ® ((Q Ú ØP) ® (Ø(P Ù P) Ú Q)))) replace proposition variable C by (Ø(P Ù P) Ú Q) in 34
36 (((Q Ú Ø(P Ù P)) ® (Ø(P Ù P) Ú Q)) ® (((Q Ú ØP) ® (Q Ú Ø(P Ù P))) ® ((Q Ú ØP) ® (Ø(P Ù P) Ú Q)))) replace proposition variable D by (Q Ú Ø(P Ù P)) in 35
37 (((Q Ú ØP) ® (Q Ú Ø(P Ù P))) ® ((Q Ú ØP) ® (Ø(P Ù P) Ú Q))) modus ponens with 29, 36
38 ((Q Ú ØP) ® (Ø(P Ù P) Ú Q)) modus ponens with 24, 37
39 ((B Ú Q) ® (Q Ú B)) replace proposition variable A by Q in 27
40 ((ØP Ú Q) ® (Q Ú ØP)) replace proposition variable B by ØP in 39
41 ((D ® C) ® (((ØP Ú Q) ® D) ® ((ØP Ú Q) ® C))) replace proposition variable B by (ØP Ú Q) in 33
42 ((D ® (Ø(P Ù P) Ú Q)) ® (((ØP Ú Q) ® D) ® ((ØP Ú Q) ® (Ø(P Ù P) Ú Q)))) replace proposition variable C by (Ø(P Ù P) Ú Q) in 41
43 (((Q Ú ØP) ® (Ø(P Ù P) Ú Q)) ® (((ØP Ú Q) ® (Q Ú ØP)) ® ((ØP Ú Q) ® (Ø(P Ù P) Ú Q)))) replace proposition variable D by (Q Ú ØP) in 42
44 (((ØP Ú Q) ® (Q Ú ØP)) ® ((ØP Ú Q) ® (Ø(P Ù P) Ú Q))) modus ponens with 38, 43
45 ((ØP Ú Q) ® (Ø(P Ù P) Ú Q)) modus ponens with 40, 44
46 ((P ® A) ® (ØP Ú A)) replace proposition variable Q by A in 9
47 ((B ® A) ® (ØB Ú A)) replace proposition variable P by B in 46
48 ((D ® C) ® (((P ® Q) ® D) ® ((P ® Q) ® C))) replace proposition variable B by (P ® Q) in 33
49 ((D ® (Ø(P Ù P) Ú Q)) ® (((P ® Q) ® D) ® ((P ® Q) ® (Ø(P Ù P) Ú Q)))) replace proposition variable C by (Ø(P Ù P) Ú Q) in 48
50 (((ØP Ú Q) ® (Ø(P Ù P) Ú Q)) ® (((P ® Q) ® (ØP Ú Q)) ® ((P ® Q) ® (Ø(P Ù P) Ú Q)))) replace proposition variable D by (ØP Ú Q) in 49
51 (((P ® Q) ® (ØP Ú Q)) ® ((P ® Q) ® (Ø(P Ù P) Ú Q))) modus ponens with 45, 50
52 ((P ® Q) ® (Ø(P Ù P) Ú Q)) modus ponens with 9, 51
53 ((ØP Ú A) ® (P ® A)) replace proposition variable Q by A in 10
54 ((ØB Ú A) ® (B ® A)) replace proposition variable P by B in 53
55 ((ØB Ú Q) ® (B ® Q)) replace proposition variable A by Q in 54
56 ((Ø(P Ù P) Ú Q) ® ((P Ù P) ® Q)) replace proposition variable B by (P Ù P) in 55
57 ((D ® ((P Ù P) ® Q)) ® (((P ® Q) ® D) ® ((P ® Q) ® ((P Ù P) ® Q)))) replace proposition variable C by ((P Ù P) ® Q) in 48
58 (((Ø(P Ù P) Ú Q) ® ((P Ù P) ® Q)) ® (((P ® Q) ® (Ø(P Ù P) Ú Q)) ® ((P ® Q) ® ((P Ù P) ® Q)))) replace proposition variable D by (Ø(P Ù P) Ú Q) in 57
59 (((P ® Q) ® (Ø(P Ù P) Ú Q)) ® ((P ® Q) ® ((P Ù P) ® Q))) modus ponens with 56, 58
60 ((P ® Q) ® ((P Ù P) ® Q)) modus ponens with 52, 59
61 ((B ® ((P Ù P) ® Q)) ® (Ø((P Ù P) ® Q) ® ØB)) replace proposition variable A by ((P Ù P) ® Q) in 13
62 (((P ® Q) ® ((P Ù P) ® Q)) ® (Ø((P Ù P) ® Q) ® Ø(P ® Q))) replace proposition variable B by (P ® Q) in 61
63 (Ø((P Ù P) ® Q) ® Ø(P ® Q)) modus ponens with 60, 62
64 ((D ® C) ® (((P ® (P ® Q)) Ú D) ® ((P ® (P ® Q)) Ú C))) replace proposition variable B by (P ® (P ® Q)) in 20
65 ((D ® Ø(P ® Q)) ® (((P ® (P ® Q)) Ú D) ® ((P ® (P ® Q)) Ú Ø(P ® Q)))) replace proposition variable C by Ø(P ® Q) in 64
66 ((Ø((P Ù P) ® Q) ® Ø(P ® Q)) ® (((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) ® ((P ® (P ® Q)) Ú Ø(P ® Q)))) replace proposition variable D by Ø((P Ù P) ® Q) in 65
67 (((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) ® ((P ® (P ® Q)) Ú Ø(P ® Q))) modus ponens with 63, 66
68 ((B Ú Ø(P ® Q)) ® (Ø(P ® Q) Ú B)) replace proposition variable A by Ø(P ® Q) in 27
69 (((P ® (P ® Q)) Ú Ø(P ® Q)) ® (Ø(P ® Q) Ú (P ® (P ® Q)))) replace proposition variable B by (P ® (P ® Q)) in 68
70 ((D ® C) ® ((((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) ® D) ® (((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) ® C))) replace proposition variable B by ((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) in 33
71 ((D ® (Ø(P ® Q) Ú (P ® (P ® Q)))) ® ((((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) ® D) ® (((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) ® (Ø(P ® Q) Ú (P ® (P ® Q)))))) replace proposition variable C by (Ø(P ® Q) Ú (P ® (P ® Q))) in 70
72 ((((P ® (P ® Q)) Ú Ø(P ® Q)) ® (Ø(P ® Q) Ú (P ® (P ® Q)))) ® ((((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) ® ((P ® (P ® Q)) Ú Ø(P ® Q))) ® (((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) ® (Ø(P ® Q) Ú (P ® (P ® Q)))))) replace proposition variable D by ((P ® (P ® Q)) Ú Ø(P ® Q)) in 71
73 ((((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) ® ((P ® (P ® Q)) Ú Ø(P ® Q))) ® (((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) ® (Ø(P ® Q) Ú (P ® (P ® Q))))) modus ponens with 69, 72
74 (((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) ® (Ø(P ® Q) Ú (P ® (P ® Q)))) modus ponens with 67, 73
75 ((B Ú (P ® (P ® Q))) ® ((P ® (P ® Q)) Ú B)) replace proposition variable A by (P ® (P ® Q)) in 27
76 ((Ø((P Ù P) ® Q) Ú (P ® (P ® Q))) ® ((P ® (P ® Q)) Ú Ø((P Ù P) ® Q))) replace proposition variable B by Ø((P Ù P) ® Q) in 75
77 ((D ® C) ® (((Ø((P Ù P) ® Q) Ú (P ® (P ® Q))) ® D) ® ((Ø((P Ù P) ® Q) Ú (P ® (P ® Q))) ® C))) replace proposition variable B by (Ø((P Ù P) ® Q) Ú (P ® (P ® Q))) in 33
78 ((D ® (Ø(P ® Q) Ú (P ® (P ® Q)))) ® (((Ø((P Ù P) ® Q) Ú (P ® (P ® Q))) ® D) ® ((Ø((P Ù P) ® Q) Ú (P ® (P ® Q))) ® (Ø(P ® Q) Ú (P ® (P ® Q)))))) replace proposition variable C by (Ø(P ® Q) Ú (P ® (P ® Q))) in 77
79 ((((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) ® (Ø(P ® Q) Ú (P ® (P ® Q)))) ® (((Ø((P Ù P) ® Q) Ú (P ® (P ® Q))) ® ((P ® (P ® Q)) Ú Ø((P Ù P) ® Q))) ® ((Ø((P Ù P) ® Q) Ú (P ® (P ® Q))) ® (Ø(P ® Q) Ú (P ® (P ® Q)))))) replace proposition variable D by ((P ® (P ® Q)) Ú Ø((P Ù P) ® Q)) in 78
80 (((Ø((P Ù P) ® Q) Ú (P ® (P ® Q))) ® ((P ® (P ® Q)) Ú Ø((P Ù P) ® Q))) ® ((Ø((P Ù P) ® Q) Ú (P ® (P ® Q))) ® (Ø(P ® Q) Ú (P ® (P ® Q))))) modus ponens with 74, 79
81 ((Ø((P Ù P) ® Q) Ú (P ® (P ® Q))) ® (Ø(P ® Q) Ú (P ® (P ® Q)))) modus ponens with 76, 80
82 ((B ® (P ® (P ® Q))) ® (ØB Ú (P ® (P ® Q)))) replace proposition variable A by (P ® (P ® Q)) in 47
83 ((((P Ù P) ® Q) ® (P ® (P ® Q))) ® (Ø((P Ù P) ® Q) Ú (P ® (P ® Q)))) replace proposition variable B by ((P Ù P) ® Q) in 82
84 ((D ® C) ® (((((P Ù P) ® Q) ® (P ® (P ® Q))) ® D) ® ((((P Ù P) ® Q) ® (P ® (P ® Q))) ® C))) replace proposition variable B by (((P Ù P) ® Q) ® (P ® (P ® Q))) in 33
85 ((D ® (Ø(P ® Q) Ú (P ® (P ® Q)))) ® (((((P Ù P) ® Q) ® (P ® (P ® Q))) ® D) ® ((((P Ù P) ® Q) ® (P ® (P ® Q))) ® (Ø(P ® Q) Ú (P ® (P ® Q)))))) replace proposition variable C by (Ø(P ® Q) Ú (P ® (P ® Q))) in 84
86 (((Ø((P Ù P) ® Q) Ú (P ® (P ® Q))) ® (Ø(P ® Q) Ú (P ® (P ® Q)))) ® (((((P Ù P) ® Q) ® (P ® (P ® Q))) ® (Ø((P Ù P) ® Q) Ú (P ® (P ® Q)))) ® ((((P Ù P) ® Q) ® (P ® (P ® Q))) ® (Ø(P ® Q) Ú (P ® (P ® Q)))))) replace proposition variable D by (Ø((P Ù P) ® Q) Ú (P ® (P ® Q))) in 85
87 (((((P Ù P) ® Q) ® (P ® (P ® Q))) ® (Ø((P Ù P) ® Q) Ú (P ® (P ® Q)))) ® ((((P Ù P) ® Q) ® (P ® (P ® Q))) ® (Ø(P ® Q) Ú (P ® (P ® Q))))) modus ponens with 81, 86
88 ((((P Ù P) ® Q) ® (P ® (P ® Q))) ® (Ø(P ® Q) Ú (P ® (P ® Q)))) modus ponens with 83, 87
89 ((ØB Ú (P ® (P ® Q))) ® (B ® (P ® (P ® Q)))) replace proposition variable A by (P ® (P ® Q)) in 54
90 ((Ø(P ® Q) Ú (P ® (P ® Q))) ® ((P ® Q) ® (P ® (P ® Q)))) replace proposition variable B by (P ® Q) in 89
91 ((D ® ((P ® Q) ® (P ® (P ® Q)))) ® (((((P Ù P) ® Q) ® (P ® (P ® Q))) ® D) ® ((((P Ù P) ® Q) ® (P ® (P ® Q))) ® ((P ® Q) ® (P ® (P ® Q)))))) replace proposition variable C by ((P ® Q) ® (P ® (P ® Q))) in 84
92 (((Ø(P ® Q) Ú (P ® (P ® Q))) ® ((P ® Q) ® (P ® (P ® Q)))) ® (((((P Ù P) ® Q) ® (P ® (P ® Q))) ® (Ø(P ® Q) Ú (P ® (P ® Q)))) ® ((((P Ù P) ® Q) ® (P ® (P ® Q))) ® ((P ® Q) ® (P ® (P ® Q)))))) replace proposition variable D by (Ø(P ® Q) Ú (P ® (P ® Q))) in 91
93 (((((P Ù P) ® Q) ® (P ® (P ® Q))) ® (Ø(P ® Q) Ú (P ® (P ® Q)))) ® ((((P Ù P) ® Q) ® (P ® (P ® Q))) ® ((P ® Q) ® (P ® (P ® Q))))) modus ponens with 90, 92
94 ((((P Ù P) ® Q) ® (P ® (P ® Q))) ® ((P ® Q) ® (P ® (P ® Q)))) modus ponens with 88, 93
95 ((P ® Q) ® (P ® (P ® Q))) modus ponens with 7, 94
qed

Cross References

This document is used by the following documents: