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:

prophilbert1_1.00.00_1.00.00.html

Is used by the following modules:

prophilbert3_1.00.00_1.00.00.html

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

This module is used by the following modules:

prophilbert3_1.00.00_1.00.00.html