for questions or link request: module admin

Further Theorems of Propositional Calculus

name: prophilbert2, module version: 1.00.00, rule version: 1.00.00, orignal: 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)

Uses the following modules:

Is used by the following modules:


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