for questions or link request: module admin

Further Theorems of Propositional Calculus

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

Description

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

References

This document uses the results of the following documents:

prophilbert2_1.00.00_1.00.00.o.html

Content

First distributive law (first direction):

1. Proposition
((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A))) (hilb36)

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	((Q Ù A) ® Q)	replace proposition variable B by Q in 3
5	((P ® Q) ® ((A Ú P) ® (A Ú Q)))	add axiom axiom4
6	((P ® Q) ® ((B Ú P) ® (B Ú Q)))	replace proposition variable A by B in 5
7	((P ® C) ® ((B Ú P) ® (B Ú C)))	replace proposition variable Q by C in 6
8	((D ® C) ® ((B Ú D) ® (B Ú C)))	replace proposition variable P by D in 7
9	((D ® C) ® ((P Ú D) ® (P Ú C)))	replace proposition variable B by P in 8
10	((D ® Q) ® ((P Ú D) ® (P Ú Q)))	replace proposition variable C by Q in 9
11	(((Q Ù A) ® Q) ® ((P Ú (Q Ù A)) ® (P Ú Q)))	replace proposition variable D by (Q Ù A) in 10
12	((P Ú (Q Ù A)) ® (P Ú Q))	modus ponens with 4, 11
13	((P Ù Q) ® Q)	add proposition hilb25
14	((P Ù A) ® A)	replace proposition variable Q by A in 13
15	((B Ù A) ® A)	replace proposition variable P by B in 14
16	((Q Ù A) ® A)	replace proposition variable B by Q in 15
17	((D ® A) ® ((P Ú D) ® (P Ú A)))	replace proposition variable C by A in 9
18	(((Q Ù A) ® A) ® ((P Ú (Q Ù A)) ® (P Ú A)))	replace proposition variable D by (Q Ù A) in 17
19	((P Ú (Q Ù A)) ® (P Ú A))	modus ponens with 16, 18
20	(P ® (Q ® (P Ù Q)))	add proposition hilb28
21	(P ® (A ® (P Ù A)))	replace proposition variable Q by A in 20
22	(B ® (A ® (B Ù A)))	replace proposition variable P by B in 21
23	(B ® ((P Ú A) ® (B Ù (P Ú A))))	replace proposition variable A by (P Ú A) in 22
24	((P Ú Q) ® ((P Ú A) ® ((P Ú Q) Ù (P Ú A))))	replace proposition variable B by (P Ú Q) in 23
25	((P ® Q) ® ((A ® P) ® (A ® Q)))	add proposition hilb1
26	((P ® Q) ® ((B ® P) ® (B ® Q)))	replace proposition variable A by B in 25
27	((P ® C) ® ((B ® P) ® (B ® C)))	replace proposition variable Q by C in 26
28	((D ® C) ® ((B ® D) ® (B ® C)))	replace proposition variable P by D in 27
29	((D ® C) ® (((P Ú (Q Ù A)) ® D) ® ((P Ú (Q Ù A)) ® C)))	replace proposition variable B by (P Ú (Q Ù A)) in 28
30	((D ® ((P Ú A) ® ((P Ú Q) Ù (P Ú A)))) ® (((P Ú (Q Ù A)) ® D) ® ((P Ú (Q Ù A)) ® ((P Ú A) ® ((P Ú Q) Ù (P Ú A))))))	replace proposition variable C by ((P Ú A) ® ((P Ú Q) Ù (P Ú A))) in 29
31	(((P Ú Q) ® ((P Ú A) ® ((P Ú Q) Ù (P Ú A)))) ® (((P Ú (Q Ù A)) ® (P Ú Q)) ® ((P Ú (Q Ù A)) ® ((P Ú A) ® ((P Ú Q) Ù (P Ú A))))))	replace proposition variable D by (P Ú Q) in 30
32	(((P Ú (Q Ù A)) ® (P Ú Q)) ® ((P Ú (Q Ù A)) ® ((P Ú A) ® ((P Ú Q) Ù (P Ú A)))))	modus ponens with 24, 31
33	((P Ú (Q Ù A)) ® ((P Ú A) ® ((P Ú Q) Ù (P Ú A))))	modus ponens with 12, 32
34	((P ® (Q ® A)) ® (Q ® (P ® A)))	add proposition hilb16
35	((P ® (Q ® B)) ® (Q ® (P ® B)))	replace proposition variable A by B in 34
36	((P ® (C ® B)) ® (C ® (P ® B)))	replace proposition variable Q by C in 35
37	((D ® (C ® B)) ® (C ® (D ® B)))	replace proposition variable P by D in 36
38	((D ® (C ® ((P Ú Q) Ù (P Ú A)))) ® (C ® (D ® ((P Ú Q) Ù (P Ú A)))))	replace proposition variable B by ((P Ú Q) Ù (P Ú A)) in 37
39	((D ® ((P Ú A) ® ((P Ú Q) Ù (P Ú A)))) ® ((P Ú A) ® (D ® ((P Ú Q) Ù (P Ú A)))))	replace proposition variable C by (P Ú A) in 38
40	(((P Ú (Q Ù A)) ® ((P Ú A) ® ((P Ú Q) Ù (P Ú A)))) ® ((P Ú A) ® ((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A)))))	replace proposition variable D by (P Ú (Q Ù A)) in 39
41	((P Ú A) ® ((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A))))	modus ponens with 33, 40
42	((D ® ((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A)))) ® (((P Ú (Q Ù A)) ® D) ® ((P Ú (Q Ù A)) ® ((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A))))))	replace proposition variable C by ((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A))) in 29
43	(((P Ú A) ® ((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A)))) ® (((P Ú (Q Ù A)) ® (P Ú A)) ® ((P Ú (Q Ù A)) ® ((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A))))))	replace proposition variable D by (P Ú A) in 42
44	(((P Ú (Q Ù A)) ® (P Ú A)) ® ((P Ú (Q Ù A)) ® ((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A)))))	modus ponens with 41, 43
45	((P Ú (Q Ù A)) ® ((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A))))	modus ponens with 19, 44
46	((P ® (P ® Q)) ® (P ® Q))	add proposition hilb33
47	((P ® (P ® A)) ® (P ® A))	replace proposition variable Q by A in 46
48	((B ® (B ® A)) ® (B ® A))	replace proposition variable P by B in 47
49	((B ® (B ® ((P Ú Q) Ù (P Ú A)))) ® (B ® ((P Ú Q) Ù (P Ú A))))	replace proposition variable A by ((P Ú Q) Ù (P Ú A)) in 48
50	(((P Ú (Q Ù A)) ® ((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A)))) ® ((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A))))	replace proposition variable B by (P Ú (Q Ù A)) in 49
51	((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A)))	modus ponens with 45, 50
	qed

First distributive law (second direction):

2. Proposition
(((P Ú Q) Ù (P Ú A)) ® (P Ú (Q Ù A))) (hilb37)

Proof:

1	(P ® (Q ® (P Ù Q)))	add proposition hilb28
2	(P ® (A ® (P Ù A)))	replace proposition variable Q by A in 1
3	(B ® (A ® (B Ù A)))	replace proposition variable P by B in 2
4	(Q ® (A ® (Q Ù A)))	replace proposition variable B by Q in 3
5	((P ® Q) ® ((A Ú P) ® (A Ú Q)))	add axiom axiom4
6	((P ® Q) ® ((B Ú P) ® (B Ú Q)))	replace proposition variable A by B in 5
7	((P ® C) ® ((B Ú P) ® (B Ú C)))	replace proposition variable Q by C in 6
8	((D ® C) ® ((B Ú D) ® (B Ú C)))	replace proposition variable P by D in 7
9	((D ® C) ® ((P Ú D) ® (P Ú C)))	replace proposition variable B by P in 8
10	((D ® (Q Ù A)) ® ((P Ú D) ® (P Ú (Q Ù A))))	replace proposition variable C by (Q Ù A) in 9
11	((A ® (Q Ù A)) ® ((P Ú A) ® (P Ú (Q Ù A))))	replace proposition variable D by A in 10
12	((P ® Q) ® ((A ® P) ® (A ® Q)))	add proposition hilb1
13	((P ® Q) ® ((B ® P) ® (B ® Q)))	replace proposition variable A by B in 12
14	((P ® C) ® ((B ® P) ® (B ® C)))	replace proposition variable Q by C in 13
15	((D ® C) ® ((B ® D) ® (B ® C)))	replace proposition variable P by D in 14
16	((D ® C) ® ((Q ® D) ® (Q ® C)))	replace proposition variable B by Q in 15
17	((D ® ((P Ú A) ® (P Ú (Q Ù A)))) ® ((Q ® D) ® (Q ® ((P Ú A) ® (P Ú (Q Ù A))))))	replace proposition variable C by ((P Ú A) ® (P Ú (Q Ù A))) in 16
18	(((A ® (Q Ù A)) ® ((P Ú A) ® (P Ú (Q Ù A)))) ® ((Q ® (A ® (Q Ù A))) ® (Q ® ((P Ú A) ® (P Ú (Q Ù A))))))	replace proposition variable D by (A ® (Q Ù A)) in 17
19	((Q ® (A ® (Q Ù A))) ® (Q ® ((P Ú A) ® (P Ú (Q Ù A)))))	modus ponens with 11, 18
20	(Q ® ((P Ú A) ® (P Ú (Q Ù A))))	modus ponens with 4, 19
21	((P ® (Q ® A)) ® (Q ® (P ® A)))	add proposition hilb16
22	((P ® (Q ® B)) ® (Q ® (P ® B)))	replace proposition variable A by B in 21
23	((P ® (C ® B)) ® (C ® (P ® B)))	replace proposition variable Q by C in 22
24	((D ® (C ® B)) ® (C ® (D ® B)))	replace proposition variable P by D in 23
25	((D ® (C ® (P Ú (Q Ù A)))) ® (C ® (D ® (P Ú (Q Ù A)))))	replace proposition variable B by (P Ú (Q Ù A)) in 24
26	((D ® ((P Ú A) ® (P Ú (Q Ù A)))) ® ((P Ú A) ® (D ® (P Ú (Q Ù A)))))	replace proposition variable C by (P Ú A) in 25
27	((Q ® ((P Ú A) ® (P Ú (Q Ù A)))) ® ((P Ú A) ® (Q ® (P Ú (Q Ù A)))))	replace proposition variable D by Q in 26
28	((P Ú A) ® (Q ® (P Ú (Q Ù A))))	modus ponens with 20, 27
29	((D ® (P Ú (Q Ù A))) ® ((P Ú D) ® (P Ú (P Ú (Q Ù A)))))	replace proposition variable C by (P Ú (Q Ù A)) in 9
30	((Q ® (P Ú (Q Ù A))) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A)))))	replace proposition variable D by Q in 29
31	((D ® C) ® (((P Ú A) ® D) ® ((P Ú A) ® C)))	replace proposition variable B by (P Ú A) in 15
32	((D ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (((P Ú A) ® D) ® ((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A)))))))	replace proposition variable C by ((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) in 31
33	(((Q ® (P Ú (Q Ù A))) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (((P Ú A) ® (Q ® (P Ú (Q Ù A)))) ® ((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A)))))))	replace proposition variable D by (Q ® (P Ú (Q Ù A))) in 32
34	(((P Ú A) ® (Q ® (P Ú (Q Ù A)))) ® ((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))))	modus ponens with 30, 33
35	((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A)))))	modus ponens with 28, 34
36	((P Ú (Q Ú A)) ® ((P Ú Q) Ú A))	add proposition hilb14
37	((P Ú (Q Ú B)) ® ((P Ú Q) Ú B))	replace proposition variable A by B in 36
38	((P Ú (C Ú B)) ® ((P Ú C) Ú B))	replace proposition variable Q by C in 37
39	((D Ú (C Ú B)) ® ((D Ú C) Ú B))	replace proposition variable P by D in 38
40	((D Ú (C Ú (Q Ù A))) ® ((D Ú C) Ú (Q Ù A)))	replace proposition variable B by (Q Ù A) in 39
41	((D Ú (P Ú (Q Ù A))) ® ((D Ú P) Ú (Q Ù A)))	replace proposition variable C by P in 40
42	((P Ú (P Ú (Q Ù A))) ® ((P Ú P) Ú (Q Ù A)))	replace proposition variable D by P in 41
43	((P ® Q) ® (ØP Ú Q))	add proposition defimpl1
44	((ØP Ú Q) ® (P ® Q))	add proposition defimpl2
45	((D ® C) ® ((Ø(P Ú Q) Ú D) ® (Ø(P Ú Q) Ú C)))	replace proposition variable B by Ø(P Ú Q) in 8
46	((D ® ((P Ú P) Ú (Q Ù A))) ® ((Ø(P Ú Q) Ú D) ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A)))))	replace proposition variable C by ((P Ú P) Ú (Q Ù A)) in 45
47	(((P Ú (P Ú (Q Ù A))) ® ((P Ú P) Ú (Q Ù A))) ® ((Ø(P Ú Q) Ú (P Ú (P Ú (Q Ù A)))) ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A)))))	replace proposition variable D by (P Ú (P Ú (Q Ù A))) in 46
48	((Ø(P Ú Q) Ú (P Ú (P Ú (Q Ù A)))) ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A))))	modus ponens with 42, 47
49	((P ® B) ® (ØP Ú B))	replace proposition variable Q by B in 43
50	((C ® B) ® (ØC Ú B))	replace proposition variable P by C in 49
51	((C ® (P Ú (P Ú (Q Ù A)))) ® (ØC Ú (P Ú (P Ú (Q Ù A)))))	replace proposition variable B by (P Ú (P Ú (Q Ù A))) in 50
52	(((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® (Ø(P Ú Q) Ú (P Ú (P Ú (Q Ù A)))))	replace proposition variable C by (P Ú Q) in 51
53	((D ® C) ® ((((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® D) ® (((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® C)))	replace proposition variable B by ((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) in 15
54	((D ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A)))) ® ((((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® D) ® (((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A))))))	replace proposition variable C by (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A))) in 53
55	(((Ø(P Ú Q) Ú (P Ú (P Ú (Q Ù A)))) ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A)))) ® ((((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® (Ø(P Ú Q) Ú (P Ú (P Ú (Q Ù A))))) ® (((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A))))))	replace proposition variable D by (Ø(P Ú Q) Ú (P Ú (P Ú (Q Ù A)))) in 54
56	((((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® (Ø(P Ú Q) Ú (P Ú (P Ú (Q Ù A))))) ® (((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A)))))	modus ponens with 48, 55
57	(((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A))))	modus ponens with 52, 56
58	((ØP Ú B) ® (P ® B))	replace proposition variable Q by B in 44
59	((ØC Ú B) ® (C ® B))	replace proposition variable P by C in 58
60	((ØC Ú ((P Ú P) Ú (Q Ù A))) ® (C ® ((P Ú P) Ú (Q Ù A))))	replace proposition variable B by ((P Ú P) Ú (Q Ù A)) in 59
61	((Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A))) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))	replace proposition variable C by (P Ú Q) in 60
62	((D ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® ((((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® D) ® (((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))))	replace proposition variable C by ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) in 53
63	(((Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A))) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® ((((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A)))) ® (((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))))	replace proposition variable D by (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A))) in 62
64	((((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A)))) ® (((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))))	modus ponens with 61, 63
65	(((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))	modus ponens with 57, 64
66	((D ® C) ® ((Ø(P Ú A) Ú D) ® (Ø(P Ú A) Ú C)))	replace proposition variable B by Ø(P Ú A) in 8
67	((D ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® ((Ø(P Ú A) Ú D) ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))))	replace proposition variable C by ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) in 66
68	((((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® ((Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))))	replace proposition variable D by ((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) in 67
69	((Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))))	modus ponens with 65, 68
70	((C ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (ØC Ú ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))))	replace proposition variable B by ((P Ú Q) ® (P Ú (P Ú (Q Ù A)))) in 50
71	(((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))))	replace proposition variable C by (P Ú A) in 70
72	((D ® C) ® ((((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® D) ® (((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® C)))	replace proposition variable B by ((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) in 15
73	((D ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))) ® ((((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® D) ® (((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))))))	replace proposition variable C by (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) in 72
74	(((Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))) ® ((((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (P Ú (Q Ù A)))))) ® (((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))))))	replace proposition variable D by (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) in 73
75	((((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (P Ú (Q Ù A)))))) ® (((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))))	modus ponens with 69, 74
76	(((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))))	modus ponens with 71, 75
77	((ØC Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (C ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))))	replace proposition variable B by ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) in 59
78	((Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® ((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))))	replace proposition variable C by (P Ú A) in 77
79	((D ® ((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))) ® ((((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® D) ® (((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® ((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))))))	replace proposition variable C by ((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) in 72
80	(((Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® ((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))) ® ((((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))) ® (((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® ((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))))))	replace proposition variable D by (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) in 79
81	((((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))) ® (((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® ((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))))	modus ponens with 78, 80
82	(((P Ú A) ® ((P Ú Q) ® (P Ú (P Ú (Q Ù A))))) ® ((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))))	modus ponens with 76, 81
83	((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))	modus ponens with 35, 82
84	((P Ú P) ® P)	add proposition hilb11
85	((D ® C) ® (((Q Ù A) Ú D) ® ((Q Ù A) Ú C)))	replace proposition variable B by (Q Ù A) in 8
86	((D ® P) ® (((Q Ù A) Ú D) ® ((Q Ù A) Ú P)))	replace proposition variable C by P in 85
87	(((P Ú P) ® P) ® (((Q Ù A) Ú (P Ú P)) ® ((Q Ù A) Ú P)))	replace proposition variable D by (P Ú P) in 86
88	(((Q Ù A) Ú (P Ú P)) ® ((Q Ù A) Ú P))	modus ponens with 84, 87
89	((P Ú Q) ® (Q Ú P))	add axiom axiom3
90	((P Ú B) ® (B Ú P))	replace proposition variable Q by B in 89
91	((C Ú B) ® (B Ú C))	replace proposition variable P by C in 90
92	((C Ú P) ® (P Ú C))	replace proposition variable B by P in 91
93	(((Q Ù A) Ú P) ® (P Ú (Q Ù A)))	replace proposition variable C by (Q Ù A) in 92
94	((D ® C) ® ((((Q Ù A) Ú (P Ú P)) ® D) ® (((Q Ù A) Ú (P Ú P)) ® C)))	replace proposition variable B by ((Q Ù A) Ú (P Ú P)) in 15
95	((D ® (P Ú (Q Ù A))) ® ((((Q Ù A) Ú (P Ú P)) ® D) ® (((Q Ù A) Ú (P Ú P)) ® (P Ú (Q Ù A)))))	replace proposition variable C by (P Ú (Q Ù A)) in 94
96	((((Q Ù A) Ú P) ® (P Ú (Q Ù A))) ® ((((Q Ù A) Ú (P Ú P)) ® ((Q Ù A) Ú P)) ® (((Q Ù A) Ú (P Ú P)) ® (P Ú (Q Ù A)))))	replace proposition variable D by ((Q Ù A) Ú P) in 95
97	((((Q Ù A) Ú (P Ú P)) ® ((Q Ù A) Ú P)) ® (((Q Ù A) Ú (P Ú P)) ® (P Ú (Q Ù A))))	modus ponens with 93, 96
98	(((Q Ù A) Ú (P Ú P)) ® (P Ú (Q Ù A)))	modus ponens with 88, 97
99	((C Ú (Q Ù A)) ® ((Q Ù A) Ú C))	replace proposition variable B by (Q Ù A) in 91
100	(((P Ú P) Ú (Q Ù A)) ® ((Q Ù A) Ú (P Ú P)))	replace proposition variable C by (P Ú P) in 99
101	((D ® C) ® ((((P Ú P) Ú (Q Ù A)) ® D) ® (((P Ú P) Ú (Q Ù A)) ® C)))	replace proposition variable B by ((P Ú P) Ú (Q Ù A)) in 15
102	((D ® (P Ú (Q Ù A))) ® ((((P Ú P) Ú (Q Ù A)) ® D) ® (((P Ú P) Ú (Q Ù A)) ® (P Ú (Q Ù A)))))	replace proposition variable C by (P Ú (Q Ù A)) in 101
103	((((Q Ù A) Ú (P Ú P)) ® (P Ú (Q Ù A))) ® ((((P Ú P) Ú (Q Ù A)) ® ((Q Ù A) Ú (P Ú P))) ® (((P Ú P) Ú (Q Ù A)) ® (P Ú (Q Ù A)))))	replace proposition variable D by ((Q Ù A) Ú (P Ú P)) in 102
104	((((P Ú P) Ú (Q Ù A)) ® ((Q Ù A) Ú (P Ú P))) ® (((P Ú P) Ú (Q Ù A)) ® (P Ú (Q Ù A))))	modus ponens with 98, 103
105	(((P Ú P) Ú (Q Ù A)) ® (P Ú (Q Ù A)))	modus ponens with 100, 104
106	((D ® (P Ú (Q Ù A))) ® ((Ø(P Ú Q) Ú D) ® (Ø(P Ú Q) Ú (P Ú (Q Ù A)))))	replace proposition variable C by (P Ú (Q Ù A)) in 45
107	((((P Ú P) Ú (Q Ù A)) ® (P Ú (Q Ù A))) ® ((Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A))) ® (Ø(P Ú Q) Ú (P Ú (Q Ù A)))))	replace proposition variable D by ((P Ú P) Ú (Q Ù A)) in 106
108	((Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A))) ® (Ø(P Ú Q) Ú (P Ú (Q Ù A))))	modus ponens with 105, 107
109	((C ® ((P Ú P) Ú (Q Ù A))) ® (ØC Ú ((P Ú P) Ú (Q Ù A))))	replace proposition variable B by ((P Ú P) Ú (Q Ù A)) in 50
110	(((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A))))	replace proposition variable C by (P Ú Q) in 109
111	((D ® C) ® ((((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® D) ® (((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® C)))	replace proposition variable B by ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) in 15
112	((D ® (Ø(P Ú Q) Ú (P Ú (Q Ù A)))) ® ((((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® D) ® (((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® (Ø(P Ú Q) Ú (P Ú (Q Ù A))))))	replace proposition variable C by (Ø(P Ú Q) Ú (P Ú (Q Ù A))) in 111
113	(((Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A))) ® (Ø(P Ú Q) Ú (P Ú (Q Ù A)))) ® ((((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A)))) ® (((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® (Ø(P Ú Q) Ú (P Ú (Q Ù A))))))	replace proposition variable D by (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A))) in 112
114	((((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® (Ø(P Ú Q) Ú ((P Ú P) Ú (Q Ù A)))) ® (((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® (Ø(P Ú Q) Ú (P Ú (Q Ù A)))))	modus ponens with 108, 113
115	(((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® (Ø(P Ú Q) Ú (P Ú (Q Ù A))))	modus ponens with 110, 114
116	((ØC Ú (P Ú (Q Ù A))) ® (C ® (P Ú (Q Ù A))))	replace proposition variable B by (P Ú (Q Ù A)) in 59
117	((Ø(P Ú Q) Ú (P Ú (Q Ù A))) ® ((P Ú Q) ® (P Ú (Q Ù A))))	replace proposition variable C by (P Ú Q) in 116
118	((D ® ((P Ú Q) ® (P Ú (Q Ù A)))) ® ((((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® D) ® (((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® ((P Ú Q) ® (P Ú (Q Ù A))))))	replace proposition variable C by ((P Ú Q) ® (P Ú (Q Ù A))) in 111
119	(((Ø(P Ú Q) Ú (P Ú (Q Ù A))) ® ((P Ú Q) ® (P Ú (Q Ù A)))) ® ((((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® (Ø(P Ú Q) Ú (P Ú (Q Ù A)))) ® (((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® ((P Ú Q) ® (P Ú (Q Ù A))))))	replace proposition variable D by (Ø(P Ú Q) Ú (P Ú (Q Ù A))) in 118
120	((((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® (Ø(P Ú Q) Ú (P Ú (Q Ù A)))) ® (((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® ((P Ú Q) ® (P Ú (Q Ù A)))))	modus ponens with 117, 119
121	(((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® ((P Ú Q) ® (P Ú (Q Ù A))))	modus ponens with 115, 120
122	((D ® ((P Ú Q) ® (P Ú (Q Ù A)))) ® ((Ø(P Ú A) Ú D) ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A))))))	replace proposition variable C by ((P Ú Q) ® (P Ú (Q Ù A))) in 66
123	((((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) ® ((P Ú Q) ® (P Ú (Q Ù A)))) ® ((Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A))))))	replace proposition variable D by ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) in 122
124	((Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A)))))	modus ponens with 121, 123
125	((C ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (ØC Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))))	replace proposition variable B by ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))) in 50
126	(((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))))	replace proposition variable C by (P Ú A) in 125
127	((D ® C) ® ((((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® D) ® (((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® C)))	replace proposition variable B by ((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) in 15
128	((D ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A))))) ® ((((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® D) ® (((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A)))))))	replace proposition variable C by (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A)))) in 127
129	(((Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A))))) ® ((((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))) ® (((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A)))))))	replace proposition variable D by (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) in 128
130	((((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (Ø(P Ú A) Ú ((P Ú Q) ® ((P Ú P) Ú (Q Ù A))))) ® (((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A))))))	modus ponens with 124, 129
131	(((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A)))))	modus ponens with 126, 130
132	((ØC Ú ((P Ú Q) ® (P Ú (Q Ù A)))) ® (C ® ((P Ú Q) ® (P Ú (Q Ù A)))))	replace proposition variable B by ((P Ú Q) ® (P Ú (Q Ù A))) in 59
133	((Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A)))) ® ((P Ú A) ® ((P Ú Q) ® (P Ú (Q Ù A)))))	replace proposition variable C by (P Ú A) in 132
134	((D ® ((P Ú A) ® ((P Ú Q) ® (P Ú (Q Ù A))))) ® ((((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® D) ® (((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® ((P Ú A) ® ((P Ú Q) ® (P Ú (Q Ù A)))))))	replace proposition variable C by ((P Ú A) ® ((P Ú Q) ® (P Ú (Q Ù A)))) in 127
135	(((Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A)))) ® ((P Ú A) ® ((P Ú Q) ® (P Ú (Q Ù A))))) ® ((((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A))))) ® (((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® ((P Ú A) ® ((P Ú Q) ® (P Ú (Q Ù A)))))))	replace proposition variable D by (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A)))) in 134
136	((((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® (Ø(P Ú A) Ú ((P Ú Q) ® (P Ú (Q Ù A))))) ® (((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® ((P Ú A) ® ((P Ú Q) ® (P Ú (Q Ù A))))))	modus ponens with 133, 135
137	(((P Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) ® ((P Ú A) ® ((P Ú Q) ® (P Ú (Q Ù A)))))	modus ponens with 131, 136
138	((P Ú A) ® ((P Ú Q) ® (P Ú (Q Ù A))))	modus ponens with 83, 137
139	((D ® ((P Ú Q) ® (P Ú (Q Ù A)))) ® ((P Ú Q) ® (D ® (P Ú (Q Ù A)))))	replace proposition variable C by (P Ú Q) in 25
140	(((P Ú A) ® ((P Ú Q) ® (P Ú (Q Ù A)))) ® ((P Ú Q) ® ((P Ú A) ® (P Ú (Q Ù A)))))	replace proposition variable D by (P Ú A) in 139
141	((P Ú Q) ® ((P Ú A) ® (P Ú (Q Ù A))))	modus ponens with 138, 140
142	((P ® (Q ® A)) ® ((P Ù Q) ® A))	add proposition hilb29
143	((P ® (Q ® B)) ® ((P Ù Q) ® B))	replace proposition variable A by B in 142
144	((P ® (C ® B)) ® ((P Ù C) ® B))	replace proposition variable Q by C in 143
145	((D ® (C ® B)) ® ((D Ù C) ® B))	replace proposition variable P by D in 144
146	((D ® (C ® (P Ú (Q Ù A)))) ® ((D Ù C) ® (P Ú (Q Ù A))))	replace proposition variable B by (P Ú (Q Ù A)) in 145
147	((D ® ((P Ú A) ® (P Ú (Q Ù A)))) ® ((D Ù (P Ú A)) ® (P Ú (Q Ù A))))	replace proposition variable C by (P Ú A) in 146
148	(((P Ú Q) ® ((P Ú A) ® (P Ú (Q Ù A)))) ® (((P Ú Q) Ù (P Ú A)) ® (P Ú (Q Ù A))))	replace proposition variable D by (P Ú Q) in 147
149	(((P Ú Q) Ù (P Ú A)) ® (P Ú (Q Ù A)))	modus ponens with 141, 148
	qed

A form for the abbreviation rule form for disjunction (first direction):

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

Proof:

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

A form for the abbreviation rule form for disjunction (second direction):

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

Proof:

1	(ØØP ® P)	add proposition hilb6
2	(ØØA ® A)	replace proposition variable P by A in 1
3	(ØØ(P Ú Q) ® (P Ú Q))	replace proposition variable A by (P Ú Q) in 2
4	((P ® Q) ® (ØP Ú Q))	add proposition defimpl1
5	((ØP Ú Q) ® (P ® Q))	add proposition defimpl2
6	((P Ú Q) ® (Q Ú P))	add axiom axiom3
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	((P ® Q) ® ((A ® P) ® (A ® Q)))	add proposition hilb1
10	((P ® Q) ® ((B ® P) ® (B ® Q)))	replace proposition variable A by B in 9
11	((P ® C) ® ((B ® P) ® (B ® C)))	replace proposition variable Q by C in 10
12	((D ® C) ® ((B ® D) ® (B ® C)))	replace proposition variable P by D in 11
13	((B Ú (P Ú Q)) ® ((P Ú Q) Ú B))	replace proposition variable A by (P Ú Q) in 8
14	((P ® A) ® (ØP Ú A))	replace proposition variable Q by A in 4
15	((B ® A) ® (ØB Ú A))	replace proposition variable P by B in 14
16	((B ® (P Ú Q)) ® (ØB Ú (P Ú Q)))	replace proposition variable A by (P Ú Q) in 15
17	((ØP Ú A) ® (P ® A))	replace proposition variable Q by A in 5
18	((ØB Ú A) ® (B ® A))	replace proposition variable P by B in 17
19	((ØB Ú (P Ú Q)) ® (B ® (P Ú Q)))	replace proposition variable A by (P Ú Q) in 18
20	(ØØQ ® Q)	replace proposition variable P by Q in 1
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) ® ((Q Ú D) ® (Q Ú C)))	replace proposition variable B by Q in 24
26	((D ® P) ® ((Q Ú D) ® (Q Ú P)))	replace proposition variable C by P in 25
27	((ØØP ® P) ® ((Q Ú ØØP) ® (Q Ú P)))	replace proposition variable D by ØØP in 26
28	((Q Ú ØØP) ® (Q Ú P))	modus ponens with 1, 27
29	((B Ú P) ® (P Ú B))	replace proposition variable A by P in 8
30	((Q Ú P) ® (P Ú Q))	replace proposition variable B by Q in 29
31	((D ® C) ® (((Q Ú ØØP) ® D) ® ((Q Ú ØØP) ® C)))	replace proposition variable B by (Q Ú ØØP) in 12
32	((D ® (P Ú Q)) ® (((Q Ú ØØP) ® D) ® ((Q Ú ØØP) ® (P Ú Q))))	replace proposition variable C by (P Ú Q) in 31
33	(((Q Ú P) ® (P Ú Q)) ® (((Q Ú ØØP) ® (Q Ú P)) ® ((Q Ú ØØP) ® (P Ú Q))))	replace proposition variable D by (Q Ú P) in 32
34	(((Q Ú ØØP) ® (Q Ú P)) ® ((Q Ú ØØP) ® (P Ú Q)))	modus ponens with 30, 33
35	((Q Ú ØØP) ® (P Ú Q))	modus ponens with 28, 34
36	((B Ú Q) ® (Q Ú B))	replace proposition variable A by Q in 8
37	((ØØP Ú Q) ® (Q Ú ØØP))	replace proposition variable B by ØØP in 36
38	((D ® C) ® (((ØØP Ú Q) ® D) ® ((ØØP Ú Q) ® C)))	replace proposition variable B by (ØØP Ú Q) in 12
39	((D ® (P Ú Q)) ® (((ØØP Ú Q) ® D) ® ((ØØP Ú Q) ® (P Ú Q))))	replace proposition variable C by (P Ú Q) in 38
40	(((Q Ú ØØP) ® (P Ú Q)) ® (((ØØP Ú Q) ® (Q Ú ØØP)) ® ((ØØP Ú Q) ® (P Ú Q))))	replace proposition variable D by (Q Ú ØØP) in 39
41	(((ØØP Ú Q) ® (Q Ú ØØP)) ® ((ØØP Ú Q) ® (P Ú Q)))	modus ponens with 35, 40
42	((ØØP Ú Q) ® (P Ú Q))	modus ponens with 37, 41
43	((P ® Q) ® (ØQ ® ØP))	add proposition hilb7
44	((P ® A) ® (ØA ® ØP))	replace proposition variable Q by A in 43
45	((B ® A) ® (ØA ® ØB))	replace proposition variable P by B in 44
46	((B ® (P Ú Q)) ® (Ø(P Ú Q) ® ØB))	replace proposition variable A by (P Ú Q) in 45
47	(((ØØP Ú Q) ® (P Ú Q)) ® (Ø(P Ú Q) ® Ø(ØØP Ú Q)))	replace proposition variable B by (ØØP Ú Q) in 46
48	(Ø(P Ú Q) ® Ø(ØØP Ú Q))	modus ponens with 42, 47
49	((B ® Ø(ØØP Ú Q)) ® (ØØ(ØØP Ú Q) ® ØB))	replace proposition variable A by Ø(ØØP Ú Q) in 45
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 45
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 24
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 8
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 12
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 13
67	((D ® C) ® (((ØØØ(P Ú Q) Ú (P Ú Q)) ® D) ® ((ØØØ(P Ú Q) Ú (P Ú Q)) ® C)))	replace proposition variable B by (ØØØ(P Ú Q) Ú (P Ú Q)) in 12
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 16
73	((D ® C) ® (((ØØ(P Ú Q) ® (P Ú Q)) ® D) ® ((ØØ(P Ú Q) ® (P Ú Q)) ® C)))	replace proposition variable B by (ØØ(P Ú Q) ® (P Ú Q)) in 12
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 19
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 3, 82
84	((D ® C) ® ((ØØP Ú D) ® (ØØP Ú C)))	replace proposition variable B by ØØP in 24
85	((D ® Q) ® ((ØØP Ú D) ® (ØØP Ú Q)))	replace proposition variable C by Q in 84
86	((ØØQ ® Q) ® ((ØØP Ú ØØQ) ® (ØØP Ú Q)))	replace proposition variable D by ØØQ in 85
87	((ØØP Ú ØØQ) ® (ØØP Ú Q))	modus ponens with 20, 86
88	((B ® (ØØP Ú Q)) ® (Ø(ØØP Ú Q) ® ØB))	replace proposition variable A by (ØØP Ú Q) in 45
89	(((ØØP Ú ØØQ) ® (ØØP Ú Q)) ® (Ø(ØØP Ú Q) ® Ø(ØØP Ú ØØQ)))	replace proposition variable B by (ØØP Ú ØØQ) in 88
90	(Ø(ØØP Ú Q) ® Ø(ØØP Ú ØØQ))	modus ponens with 87, 89
91	((B ® Ø(ØØP Ú ØØQ)) ® (ØØ(ØØP Ú ØØQ) ® ØB))	replace proposition variable A by Ø(ØØP Ú ØØQ) in 45
92	((Ø(ØØP Ú Q) ® Ø(ØØP Ú ØØQ)) ® (ØØ(ØØP Ú ØØQ) ® ØØ(ØØP Ú Q)))	replace proposition variable B by Ø(ØØP Ú Q) in 91
93	(ØØ(ØØP Ú ØØQ) ® ØØ(ØØP Ú Q))	modus ponens with 90, 92
94	((B ® ØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú Q) ® ØB))	replace proposition variable A by ØØ(ØØP Ú Q) in 45
95	((ØØ(ØØP Ú ØØQ) ® ØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú Q) ® ØØØ(ØØP Ú ØØQ)))	replace proposition variable B by ØØ(ØØP Ú ØØQ) in 94
96	(ØØØ(ØØP Ú Q) ® ØØØ(ØØP Ú ØØQ))	modus ponens with 93, 95
97	((D ® ØØØ(ØØP Ú ØØQ)) ® (((P Ú Q) Ú D) ® ((P Ú Q) Ú ØØØ(ØØP Ú ØØQ))))	replace proposition variable C by ØØØ(ØØP Ú ØØQ) in 55
98	((ØØØ(ØØP Ú Q) ® ØØØ(ØØP Ú ØØQ)) ® (((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú ØØQ))))	replace proposition variable D by ØØØ(ØØP Ú Q) in 97
99	(((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú ØØQ)))	modus ponens with 96, 98
100	((B Ú ØØØ(ØØP Ú ØØQ)) ® (ØØØ(ØØP Ú ØØQ) Ú B))	replace proposition variable A by ØØØ(ØØP Ú ØØQ) in 8
101	(((P Ú Q) Ú ØØØ(ØØP Ú ØØQ)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q)))	replace proposition variable B by (P Ú Q) in 100
102	((D ® C) ® ((((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® D) ® (((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® C)))	replace proposition variable B by ((P Ú Q) Ú ØØØ(ØØP Ú Q)) in 12
103	((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 102
104	((((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 103
105	((((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú ØØQ))) ® (((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))))	modus ponens with 101, 104
106	(((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q)))	modus ponens with 99, 105
107	((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú Q)))	replace proposition variable B by ØØØ(ØØP Ú Q) in 13
108	((D ® C) ® (((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® D) ® ((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® C)))	replace proposition variable B by (ØØØ(ØØP Ú Q) Ú (P Ú Q)) in 12
109	((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 108
110	((((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 109
111	(((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú Q))) ® ((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))))	modus ponens with 106, 110
112	((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q)))	modus ponens with 107, 111
113	((ØØ(ØØP Ú Q) ® (P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q)))	replace proposition variable B by ØØ(ØØP Ú Q) in 16
114	((D ® C) ® (((ØØ(ØØP Ú Q) ® (P Ú Q)) ® D) ® ((ØØ(ØØP Ú Q) ® (P Ú Q)) ® C)))	replace proposition variable B by (ØØ(ØØP Ú Q) ® (P Ú Q)) in 12
115	((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 114
116	(((ØØØ(ØØ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 115
117	(((ØØ(ØØP Ú Q) ® (P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))) ® ((ØØ(ØØP Ú Q) ® (P Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))))	modus ponens with 112, 116
118	((ØØ(ØØP Ú Q) ® (P Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q)))	modus ponens with 113, 117
119	((ØØØ(ØØP Ú ØØQ) Ú (P Ú Q)) ® (ØØ(ØØP Ú ØØQ) ® (P Ú Q)))	replace proposition variable B by ØØ(ØØP Ú ØØQ) in 19
120	((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 114
121	(((ØØØ(ØØ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 120
122	(((ØØ(ØØP Ú Q) ® (P Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))) ® ((ØØ(ØØP Ú Q) ® (P Ú Q)) ® (ØØ(ØØP Ú ØØQ) ® (P Ú Q))))	modus ponens with 119, 121
123	((ØØ(ØØP Ú Q) ® (P Ú Q)) ® (ØØ(ØØP Ú ØØQ) ® (P Ú Q)))	modus ponens with 118, 122
124	(ØØ(ØØP Ú ØØQ) ® (P Ú Q))	modus ponens with 83, 123
125	(Ø(ØP Ù ØQ) ® (P Ú Q))	reverse abbreviation and in 124 at occurence 1
	qed

By duality we get the second distributive law (first direction):

5. Proposition
((P Ù (Q Ú A)) ® ((P Ù Q) Ú (P Ù A))) (hilb40)

Proof:

1	(((P Ú Q) Ù (P Ú A)) ® (P Ú (Q Ù A)))	add proposition hilb37
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) Ù (P Ú A)) ® (P Ú (Q Ù A))) ® (Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))))	replace proposition variable B by ((P Ú Q) Ù (P Ú A)) in 5
7	(Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú 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) Ù (P Ú A)) Ú D) ® (Ø((P Ú Q) Ù (P Ú A)) Ú C)))	replace proposition variable B by Ø((P Ú Q) Ù (P Ú A)) in 14
30	((D ® ØØ(P Ú ØØ(Q Ù A))) ® ((Ø((P Ú Q) Ù (P Ú A)) Ú D) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A)))))	replace proposition variable C by ØØ(P Ú ØØ(Q Ù A)) in 29
31	((ØØ(P Ú (Q Ù A)) ® ØØ(P Ú ØØ(Q Ù A))) ® ((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A)))))	replace proposition variable D by ØØ(P Ú (Q Ù A)) in 30
32	((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú 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) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))))	replace proposition variable C by Ø((P Ú Q) Ù (P Ú 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) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® D) ® ((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® C)))	replace proposition variable B by (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) in 41
43	((D ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® (((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® D) ® ((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))))))	replace proposition variable C by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 42
44	(((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® (((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A)))) ® ((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))))))	replace proposition variable D by (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A))) in 43
45	(((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A)))) ® ((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))))	modus ponens with 37, 44
46	((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))))	modus ponens with 32, 45
47	((C Ú Ø((P Ú Q) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú C))	replace proposition variable B by Ø((P Ú Q) Ù (P Ú A)) in 35
48	((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))))	replace proposition variable C by ØØ(P Ú (Q Ù A)) in 47
49	((D ® C) ® (((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® C)))	replace proposition variable B by (ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 41
50	((D ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® (((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))))))	replace proposition variable C by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 49
51	(((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® (((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A)))) ® ((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))))))	replace proposition variable D by (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) in 50
52	(((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A)))) ® ((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))))	modus ponens with 46, 51
53	((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú 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) Ù (P Ú A))) ® (ØC Ú Ø((P Ú Q) Ù (P Ú A))))	replace proposition variable B by Ø((P Ú Q) Ù (P Ú A)) in 55
57	((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))))	replace proposition variable C by Ø(P Ú (Q Ù A)) in 56
58	((D ® C) ® (((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® C)))	replace proposition variable B by (Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) in 41
59	((D ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))))))	replace proposition variable C by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 58
60	(((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))))))	replace proposition variable D by (ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 59
61	(((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))))	modus ponens with 53, 60
62	((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú 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) Ù (P Ú A))) ® (C ® Ø((P Ú Q) Ù (P Ú A))))	replace proposition variable B by Ø((P Ú Q) Ù (P Ú A)) in 64
66	((ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))))	replace proposition variable C by Ø(P Ú ØØ(Q Ù A)) in 65
67	((D ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))))))	replace proposition variable C by (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) in 58
68	(((ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))))))	replace proposition variable D by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 67
69	(((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A)))))	modus ponens with 66, 68
70	((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))))	modus ponens with 62, 69
71	(Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú 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	((P Ù Q) ® Ø(ØP Ú ØQ))	add proposition defand1
76	(Ø(ØP Ú ØQ) ® (P Ù Q))	add proposition defand2
77	((B ® (P Ú Q)) ® (Ø(P Ú Q) ® ØB))	replace proposition variable A by (P Ú Q) in 4
78	((ØØ(P Ú Q) ® (P Ú Q)) ® (Ø(P Ú Q) ® ØØØ(P Ú Q)))	replace proposition variable B by ØØ(P Ú Q) in 77
79	(Ø(P Ú Q) ® ØØØ(P Ú Q))	modus ponens with 74, 78
80	((D ® C) ® ((Ø(P Ú A) Ú D) ® (Ø(P Ú A) Ú C)))	replace proposition variable B by Ø(P Ú A) in 14
81	((D ® ØØØ(P Ú Q)) ® ((Ø(P Ú A) Ú D) ® (Ø(P Ú A) Ú ØØØ(P Ú Q))))	replace proposition variable C by ØØØ(P Ú Q) in 80
82	((Ø(P Ú Q) ® ØØØ(P Ú Q)) ® ((Ø(P Ú A) Ú Ø(P Ú Q)) ® (Ø(P Ú A) Ú ØØØ(P Ú Q))))	replace proposition variable D by Ø(P Ú Q) in 81
83	((Ø(P Ú A) Ú Ø(P Ú Q)) ® (Ø(P Ú A) Ú ØØØ(P Ú Q)))	modus ponens with 79, 82
84	((C Ú ØØØ(P Ú Q)) ® (ØØØ(P Ú Q) Ú C))	replace proposition variable B by ØØØ(P Ú Q) in 35
85	((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A)))	replace proposition variable C by Ø(P Ú A) in 84
86	((D ® C) ® (((Ø(P Ú A) Ú Ø(P Ú Q)) ® D) ® ((Ø(P Ú A) Ú Ø(P Ú Q)) ® C)))	replace proposition variable B by (Ø(P Ú A) Ú Ø(P Ú Q)) in 41
87	((D ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((Ø(P Ú A) Ú Ø(P Ú Q)) ® D) ® ((Ø(P Ú A) Ú Ø(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable C by (ØØØ(P Ú Q) Ú Ø(P Ú A)) in 86
88	(((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((Ø(P Ú A) Ú Ø(P Ú Q)) ® (Ø(P Ú A) Ú ØØØ(P Ú Q))) ® ((Ø(P Ú A) Ú Ø(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable D by (Ø(P Ú A) Ú ØØØ(P Ú Q)) in 87
89	(((Ø(P Ú A) Ú Ø(P Ú Q)) ® (Ø(P Ú A) Ú ØØØ(P Ú Q))) ® ((Ø(P Ú A) Ú Ø(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))))	modus ponens with 85, 88
90	((Ø(P Ú A) Ú Ø(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A)))	modus ponens with 83, 89
91	((C Ú Ø(P Ú A)) ® (Ø(P Ú A) Ú C))	replace proposition variable B by Ø(P Ú A) in 35
92	((Ø(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú A) Ú Ø(P Ú Q)))	replace proposition variable C by Ø(P Ú Q) in 91
93	((D ® C) ® (((Ø(P Ú Q) Ú Ø(P Ú A)) ® D) ® ((Ø(P Ú Q) Ú Ø(P Ú A)) ® C)))	replace proposition variable B by (Ø(P Ú Q) Ú Ø(P Ú A)) in 41
94	((D ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((Ø(P Ú Q) Ú Ø(P Ú A)) ® D) ® ((Ø(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable C by (ØØØ(P Ú Q) Ú Ø(P Ú A)) in 93
95	(((Ø(P Ú A) Ú Ø(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((Ø(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú A) Ú Ø(P Ú Q))) ® ((Ø(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable D by (Ø(P Ú A) Ú Ø(P Ú Q)) in 94
96	(((Ø(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú A) Ú Ø(P Ú Q))) ® ((Ø(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))))	modus ponens with 90, 95
97	((Ø(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A)))	modus ponens with 92, 96
98	((C ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® ØC))	replace proposition variable B by (ØØØ(P Ú Q) Ú Ø(P Ú A)) in 20
99	(((Ø(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))))	replace proposition variable C by (Ø(P Ú Q) Ú Ø(P Ú A)) in 98
100	(Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A)))	modus ponens with 97, 99
101	((P Ù B) ® Ø(ØP Ú ØB))	replace proposition variable Q by B in 75
102	((C Ù B) ® Ø(ØC Ú ØB))	replace proposition variable P by C in 101
103	((C Ù (P Ú A)) ® Ø(ØC Ú Ø(P Ú A)))	replace proposition variable B by (P Ú A) in 102
104	((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)))	replace proposition variable C by ØØ(P Ú Q) in 103
105	((D ® C) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® C)))	replace proposition variable B by (ØØ(P Ú Q) Ù (P Ú A)) in 41
106	((D ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable C by Ø(Ø(P Ú Q) Ú Ø(P Ú A)) in 105
107	((Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable D by Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) in 106
108	(((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))))	modus ponens with 100, 107
109	((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A)))	modus ponens with 104, 108
110	(Ø(ØP Ú ØB) ® (P Ù B))	replace proposition variable Q by B in 76
111	(Ø(ØC Ú ØB) ® (C Ù B))	replace proposition variable P by C in 110
112	(Ø(ØC Ú Ø(P Ú A)) ® (C Ù (P Ú A)))	replace proposition variable B by (P Ú A) in 111
113	(Ø(Ø(P Ú Q) Ú Ø(P Ú A)) ® ((P Ú Q) Ù (P Ú A)))	replace proposition variable C by (P Ú Q) in 112
114	((D ® ((P Ú Q) Ù (P Ú A))) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® ((P Ú Q) Ù (P Ú A)))))	replace proposition variable C by ((P Ú Q) Ù (P Ú A)) in 105
115	((Ø(Ø(P Ú Q) Ú Ø(P Ú A)) ® ((P Ú Q) Ù (P Ú A))) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® ((P Ú Q) Ù (P Ú A)))))	replace proposition variable D by Ø(Ø(P Ú Q) Ú Ø(P Ú A)) in 114
116	(((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® ((P Ú Q) Ù (P Ú A))))	modus ponens with 113, 115
117	((ØØ(P Ú Q) Ù (P Ú A)) ® ((P Ú Q) Ù (P Ú A)))	modus ponens with 109, 116
118	((C ® ((P Ú Q) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) ® ØC))	replace proposition variable B by ((P Ú Q) Ù (P Ú A)) in 20
119	(((ØØ(P Ú Q) Ù (P Ú A)) ® ((P Ú Q) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))))	replace proposition variable C by (ØØ(P Ú Q) Ù (P Ú A)) in 118
120	(Ø((P Ú Q) Ù (P Ú A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A)))	modus ponens with 117, 119
121	((D ® C) ® ((ØØ(P Ú ØØ(Q Ù A)) Ú D) ® (ØØ(P Ú ØØ(Q Ù A)) Ú C)))	replace proposition variable B by ØØ(P Ú ØØ(Q Ù A)) in 14
122	((D ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® ((ØØ(P Ú ØØ(Q Ù A)) Ú D) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))))	replace proposition variable C by Ø(ØØ(P Ú Q) Ù (P Ú A)) in 121
123	((Ø((P Ú Q) Ù (P Ú A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® ((ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))))	replace proposition variable D by Ø((P Ú Q) Ù (P Ú A)) in 122
124	((ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))))	modus ponens with 120, 123
125	((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))))	replace proposition variable C by Ø(P Ú ØØ(Q Ù A)) in 56
126	((D ® C) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® C)))	replace proposition variable B by (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) in 41
127	((D ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))))))	replace proposition variable C by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) in 126
128	(((ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))))))	replace proposition variable D by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 127
129	(((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))))	modus ponens with 124, 128
130	((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))))	modus ponens with 125, 129
131	((ØC Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (C ® Ø(ØØ(P Ú Q) Ù (P Ú A))))	replace proposition variable B by Ø(ØØ(P Ú Q) Ù (P Ú A)) in 64
132	((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))))	replace proposition variable C by Ø(P Ú ØØ(Q Ù A)) in 131
133	((D ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))))))	replace proposition variable C by (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) in 126
134	(((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))))))	replace proposition variable D by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) in 133
135	(((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A)))))	modus ponens with 132, 134
136	((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))))	modus ponens with 130, 135
137	(Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A)))	modus ponens with 71, 136
138	(ØØB ® B)	replace proposition variable P by B in 72
139	(ØØ(P Ú A) ® (P Ú A))	replace proposition variable B by (P Ú A) in 138
140	((C ® (P Ú A)) ® (Ø(P Ú A) ® ØC))	replace proposition variable B by (P Ú A) in 20
141	((ØØ(P Ú A) ® (P Ú A)) ® (Ø(P Ú A) ® ØØØ(P Ú A)))	replace proposition variable C by ØØ(P Ú A) in 140
142	(Ø(P Ú A) ® ØØØ(P Ú A))	modus ponens with 139, 141
143	((D ® C) ® ((ØØØ(P Ú Q) Ú D) ® (ØØØ(P Ú Q) Ú C)))	replace proposition variable B by ØØØ(P Ú Q) in 14
144	((D ® ØØØ(P Ú A)) ® ((ØØØ(P Ú Q) Ú D) ® (ØØØ(P Ú Q) Ú ØØØ(P Ú A))))	replace proposition variable C by ØØØ(P Ú A) in 143
145	((Ø(P Ú A) ® ØØØ(P Ú A)) ® ((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú ØØØ(P Ú A))))	replace proposition variable D by Ø(P Ú A) in 144
146	((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú ØØØ(P Ú A)))	modus ponens with 142, 145
147	((C ® (ØØØ(P Ú Q) Ú ØØØ(P Ú A))) ® (Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) ® ØC))	replace proposition variable B by (ØØØ(P Ú Q) Ú ØØØ(P Ú A)) in 20
148	(((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú ØØØ(P Ú A))) ® (Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))))	replace proposition variable C by (ØØØ(P Ú Q) Ú Ø(P Ú A)) in 147
149	(Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)))	modus ponens with 146, 148
150	((C Ù ØØ(P Ú A)) ® Ø(ØC Ú ØØØ(P Ú A)))	replace proposition variable B by ØØ(P Ú A) in 102
151	((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)))	replace proposition variable C by ØØ(P Ú Q) in 150
152	((D ® C) ® (((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® C)))	replace proposition variable B by (ØØ(P Ú Q) Ù ØØ(P Ú A)) in 41
153	((D ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable C by Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) in 152
154	((Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A))) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable D by Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) in 153
155	(((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A))) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))))	modus ponens with 149, 154
156	((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)))	modus ponens with 151, 155
157	(Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A)))	replace proposition variable C by ØØ(P Ú Q) in 112
158	((D ® (ØØ(P Ú Q) Ù (P Ú A))) ® (((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A)))))	replace proposition variable C by (ØØ(P Ú Q) Ù (P Ú A)) in 152
159	((Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A))) ® (((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A)))))	replace proposition variable D by Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) in 158
160	(((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A))))	modus ponens with 157, 159
161	((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A)))	modus ponens with 156, 160
162	((C ® (ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® ØC))	replace proposition variable B by (ØØ(P Ú Q) Ù (P Ú A)) in 20
163	(((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))	replace proposition variable C by (ØØ(P Ú Q) Ù ØØ(P Ú A)) in 162
164	(Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))	modus ponens with 161, 163
165	((D ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® ((ØØ(P Ú ØØ(Q Ù A)) Ú D) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))))	replace proposition variable C by Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) in 121
166	((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® ((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))))	replace proposition variable D by Ø(ØØ(P Ú Q) Ù (P Ú A)) in 165
167	((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))	modus ponens with 164, 166
168	((C ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØC Ú Ø(ØØ(P Ú Q) Ù (P Ú A))))	replace proposition variable B by Ø(ØØ(P Ú Q) Ù (P Ú A)) in 55
169	((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))))	replace proposition variable C by Ø(P Ú ØØ(Q Ù A)) in 168
170	((D ® C) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® C)))	replace proposition variable B by (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) in 41
171	((D ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))))	replace proposition variable C by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) in 170
172	(((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))))	replace proposition variable D by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) in 171
173	(((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))))	modus ponens with 167, 172
174	((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))	modus ponens with 169, 173
175	((ØC Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® (C ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))	replace proposition variable B by Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) in 64
176	((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))	replace proposition variable C by Ø(P Ú ØØ(Q Ù A)) in 175
177	((D ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))))	replace proposition variable C by (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) in 170
178	(((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))))	replace proposition variable D by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) in 177
179	(((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))))	modus ponens with 176, 178
180	((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))	modus ponens with 174, 179
181	(Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))	modus ponens with 137, 180
182	(Ø(P Ú ØØ(Q Ù B)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú B)))	replace proposition variable A by B in 181
183	(Ø(P Ú ØØ(C Ù B)) ® Ø(ØØ(P Ú C) Ù ØØ(P Ú B)))	replace proposition variable Q by C in 182
184	(Ø(D Ú ØØ(C Ù B)) ® Ø(ØØ(D Ú C) Ù ØØ(D Ú B)))	replace proposition variable P by D in 183
185	(Ø(D Ú ØØ(C Ù ØA)) ® Ø(ØØ(D Ú C) Ù ØØ(D Ú ØA)))	replace proposition variable B by ØA in 184
186	(Ø(D Ú ØØ(ØQ Ù ØA)) ® Ø(ØØ(D Ú ØQ) Ù ØØ(D Ú ØA)))	replace proposition variable C by ØQ in 185
187	(Ø(ØP Ú ØØ(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))	replace proposition variable D by ØP in 186
188	((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))	reverse abbreviation and in 187 at occurence 1
189	((P Ú Q) ® Ø(ØP Ù ØQ))	add proposition hilb38
190	((P Ú B) ® Ø(ØP Ù ØB))	replace proposition variable Q by B in 189
191	((C Ú B) ® Ø(ØC Ù ØB))	replace proposition variable P by C in 190
192	((C Ú A) ® Ø(ØC Ù ØA))	replace proposition variable B by A in 191
193	((Q Ú A) ® Ø(ØQ Ù ØA))	replace proposition variable C by Q in 192
194	((C ® Ø(ØQ Ù ØA)) ® (ØØ(ØQ Ù ØA) ® ØC))	replace proposition variable B by Ø(ØQ Ù ØA) in 20
195	(((Q Ú A) ® Ø(ØQ Ù ØA)) ® (ØØ(ØQ Ù ØA) ® Ø(Q Ú A)))	replace proposition variable C by (Q Ú A) in 194
196	(ØØ(ØQ Ù ØA) ® Ø(Q Ú A))	modus ponens with 193, 195
197	((D ® C) ® ((ØP Ú D) ® (ØP Ú C)))	replace proposition variable B by ØP in 14
198	((D ® Ø(Q Ú A)) ® ((ØP Ú D) ® (ØP Ú Ø(Q Ú A))))	replace proposition variable C by Ø(Q Ú A) in 197
199	((ØØ(ØQ Ù ØA) ® Ø(Q Ú A)) ® ((ØP Ú ØØ(ØQ Ù ØA)) ® (ØP Ú Ø(Q Ú A))))	replace proposition variable D by ØØ(ØQ Ù ØA) in 198
200	((ØP Ú ØØ(ØQ Ù ØA)) ® (ØP Ú Ø(Q Ú A)))	modus ponens with 196, 199
201	((C ® (ØP Ú Ø(Q Ú A))) ® (Ø(ØP Ú Ø(Q Ú A)) ® ØC))	replace proposition variable B by (ØP Ú Ø(Q Ú A)) in 20
202	(((ØP Ú ØØ(ØQ Ù ØA)) ® (ØP Ú Ø(Q Ú A))) ® (Ø(ØP Ú Ø(Q Ú A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA))))	replace proposition variable C by (ØP Ú ØØ(ØQ Ù ØA)) in 201
203	(Ø(ØP Ú Ø(Q Ú A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA)))	modus ponens with 200, 202
204	((C Ù (Q Ú A)) ® Ø(ØC Ú Ø(Q Ú A)))	replace proposition variable B by (Q Ú A) in 102
205	((P Ù (Q Ú A)) ® Ø(ØP Ú Ø(Q Ú A)))	replace proposition variable C by P in 204
206	((D ® C) ® (((P Ù (Q Ú A)) ® D) ® ((P Ù (Q Ú A)) ® C)))	replace proposition variable B by (P Ù (Q Ú A)) in 41
207	((D ® Ø(ØP Ú ØØ(ØQ Ù ØA))) ® (((P Ù (Q Ú A)) ® D) ® ((P Ù (Q Ú A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA)))))	replace proposition variable C by Ø(ØP Ú ØØ(ØQ Ù ØA)) in 206
208	((Ø(Ø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 207
209	(((P Ù (Q Ú A)) ® Ø(ØP Ú Ø(Q Ú A))) ® ((P Ù (Q Ú A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA))))	modus ponens with 203, 208
210	((P Ù (Q Ú A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA)))	modus ponens with 205, 209
211	(Ø(ØC Ú ØØ(ØQ Ù ØA)) ® (C Ù Ø(ØQ Ù ØA)))	replace proposition variable B by Ø(ØQ Ù ØA) in 111
212	(Ø(ØP Ú ØØ(ØQ Ù ØA)) ® (P Ù Ø(ØQ Ù ØA)))	replace proposition variable C by P in 211
213	((D ® (P Ù Ø(ØQ Ù ØA))) ® (((P Ù (Q Ú A)) ® D) ® ((P Ù (Q Ú A)) ® (P Ù Ø(ØQ Ù ØA)))))	replace proposition variable C by (P Ù Ø(ØQ Ù ØA)) in 206
214	((Ø(Ø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 213
215	(((P Ù (Q Ú A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA))) ® ((P Ù (Q Ú A)) ® (P Ù Ø(ØQ Ù ØA))))	modus ponens with 212, 214
216	((P Ù (Q Ú A)) ® (P Ù Ø(ØQ Ù ØA)))	modus ponens with 210, 215
217	((C ® (P Ù Ø(ØQ Ù ØA))) ® (Ø(P Ù Ø(ØQ Ù ØA)) ® ØC))	replace proposition variable B by (P Ù Ø(ØQ Ù ØA)) in 20
218	(((P Ù (Q Ú A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø(P Ù Ø(ØQ Ù ØA)) ® Ø(P Ù (Q Ú A))))	replace proposition variable C by (P Ù (Q Ú A)) in 217
219	(Ø(P Ù Ø(ØQ Ù ØA)) ® Ø(P Ù (Q Ú A)))	modus ponens with 216, 218
220	((D ® C) ® ((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú D) ® (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú C)))	replace proposition variable B by Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) in 14
221	((D ® Ø(P Ù (Q Ú A))) ® ((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú D) ® (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù (Q Ú A)))))	replace proposition variable C by Ø(P Ù (Q Ú A)) in 220
222	((Ø(P Ù Ø(ØQ Ù ØA)) ® Ø(P Ù (Q Ú A))) ® ((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù (Q Ú A)))))	replace proposition variable D by Ø(P Ù Ø(ØQ Ù ØA)) in 221
223	((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù (Q Ú A))))	modus ponens with 219, 222
224	((C Ú Ø(P Ù (Q Ú A))) ® (Ø(P Ù (Q Ú A)) Ú C))	replace proposition variable B by Ø(P Ù (Q Ú A)) in 35
225	((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù (Q Ú A))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))	replace proposition variable C by Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) in 224
226	((D ® C) ® (((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® D) ® ((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® C)))	replace proposition variable B by (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) in 41
227	((D ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® (((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® D) ® ((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))))	replace proposition variable C by (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) in 226
228	(((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù (Q Ú A))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® (((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù (Q Ú A)))) ® ((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))))	replace proposition variable D by (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù (Q Ú A))) in 227
229	(((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù (Q Ú A)))) ® ((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))))	modus ponens with 225, 228
230	((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))	modus ponens with 223, 229
231	((C Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú C))	replace proposition variable B by Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) in 35
232	((Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))))	replace proposition variable C by Ø(P Ù Ø(ØQ Ù ØA)) in 231
233	((D ® C) ® (((Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® D) ® ((Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® C)))	replace proposition variable B by (Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) in 41
234	((D ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® (((Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® D) ® ((Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))))	replace proposition variable C by (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) in 233
235	(((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® (((Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA)))) ® ((Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))))	replace proposition variable D by (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) in 234
236	(((Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA)))) ® ((Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))))	modus ponens with 230, 235
237	((Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))	modus ponens with 232, 236
238	((C ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (ØC Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))	replace proposition variable B by Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) in 55
239	(((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))	replace proposition variable C by (P Ù Ø(ØQ Ù ØA)) in 238
240	((D ® C) ® ((((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® D) ® (((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® C)))	replace proposition variable B by ((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) in 41
241	((D ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® ((((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® D) ® (((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))))	replace proposition variable C by (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) in 240
242	(((Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® ((((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® (((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))))	replace proposition variable D by (Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) in 241
243	((((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù Ø(ØQ Ù ØA)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® (((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))))	modus ponens with 237, 242
244	(((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))	modus ponens with 239, 243
245	((ØC Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (C ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))	replace proposition variable B by Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) in 64
246	((Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® ((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))	replace proposition variable C by (P Ù (Q Ú A)) in 245
247	((D ® ((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® ((((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® D) ® (((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® ((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))))	replace proposition variable C by ((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) in 240
248	(((Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® ((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® ((((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® (((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® ((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))))	replace proposition variable D by (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) in 247
249	((((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® (((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® ((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))))	modus ponens with 246, 248
250	(((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® ((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))	modus ponens with 244, 249
251	((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))	modus ponens with 188, 250
252	(Ø(ØP Ù ØQ) ® (P Ú Q))	add proposition hilb39
253	(Ø(ØP Ù ØB) ® (P Ú B))	replace proposition variable Q by B in 252
254	(Ø(ØC Ù ØB) ® (C Ú B))	replace proposition variable P by C in 253
255	(Ø(ØC Ù ØØ(ØP Ú ØA)) ® (C Ú Ø(ØP Ú ØA)))	replace proposition variable B by Ø(ØP Ú ØA) in 254
256	(Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)))	replace proposition variable C by Ø(ØP Ú ØQ) in 255
257	((D ® C) ® ((Ø(P Ù (Q Ú A)) Ú D) ® (Ø(P Ù (Q Ú A)) Ú C)))	replace proposition variable B by Ø(P Ù (Q Ú A)) in 14
258	((D ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))) ® ((Ø(P Ù (Q Ú A)) Ú D) ® (Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)))))	replace proposition variable C by (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)) in 257
259	((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))) ® ((Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)))))	replace proposition variable D by Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) in 258
260	((Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))))	modus ponens with 256, 259
261	(((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))))	replace proposition variable C by (P Ù (Q Ú A)) in 238
262	((D ® C) ® ((((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® D) ® (((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® C)))	replace proposition variable B by ((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) in 41
263	((D ® (Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)))) ® ((((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® D) ® (((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))))))	replace proposition variable C by (Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))) in 262
264	(((Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)))) ® ((((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® (((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))))))	replace proposition variable D by (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) in 263
265	((((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)))) ® (((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)))))	modus ponens with 260, 264
266	(((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))))	modus ponens with 261, 265
267	((ØC Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))) ® (C ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))))	replace proposition variable B by (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)) in 64
268	((Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))) ® ((P Ù (Q Ú A)) ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))))	replace proposition variable C by (P Ù (Q Ú A)) in 267
269	((D ® ((P Ù (Q Ú A)) ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)))) ® ((((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® D) ® (((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® ((P Ù (Q Ú A)) ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))))))	replace proposition variable C by ((P Ù (Q Ú A)) ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))) in 262
270	(((Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))) ® ((P Ù (Q Ú A)) ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)))) ® ((((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)))) ® (((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® ((P Ù (Q Ú A)) ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))))))	replace proposition variable D by (Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))) in 269
271	((((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® (Ø(P Ù (Q Ú A)) Ú (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)))) ® (((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® ((P Ù (Q Ú A)) ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)))))	modus ponens with 268, 270
272	(((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ® ((P Ù (Q Ú A)) ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))))	modus ponens with 266, 271
273	((P Ù (Q Ú A)) ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA)))	modus ponens with 251, 272
274	((P Ù (Q Ú A)) ® ((P Ù Q) Ú Ø(ØP Ú ØA)))	reverse abbreviation and in 273 at occurence 1
275	((P Ù (Q Ú A)) ® ((P Ù Q) Ú (P Ù A)))	reverse abbreviation and in 274 at occurence 1
	qed

The second distributive law (second direction):

6. Proposition
(((P Ù Q) Ú (P Ù A)) ® (P Ù (Q Ú A))) (hilb41)

Proof:

1	((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A)))	add proposition hilb36
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) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) ® ØB))	replace proposition variable A by ((P Ú Q) Ù (P Ú A)) in 4
6	(((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))))	replace proposition variable B by (P Ú (Q Ù A)) in 5
7	(Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A)))	modus ponens with 1, 6
8	(ØØP ® P)	add proposition hilb6
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	((D ® C) ® ((ØØ((P Ú Q) Ù (P Ú A)) Ú D) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú C)))	replace proposition variable B by ØØ((P Ú Q) Ù (P Ú A)) in 14
27	((D ® Ø(P Ú ØØ(Q Ù A))) ® ((ØØ((P Ú Q) Ù (P Ú A)) Ú D) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))))	replace proposition variable C by Ø(P Ú ØØ(Q Ù A)) in 26
28	((Ø(P Ú (Q Ù A)) ® Ø(P Ú ØØ(Q Ù A))) ® ((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú (Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))))	replace proposition variable D by Ø(P Ú (Q Ù A)) in 27
29	((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú (Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))	modus ponens with 23, 28
30	((P ® B) ® (ØP Ú B))	replace proposition variable Q by B in 24
31	((C ® B) ® (ØC Ú B))	replace proposition variable P by C in 30
32	((C ® Ø(P Ú (Q Ù A))) ® (ØC Ú Ø(P Ú (Q Ù A))))	replace proposition variable B by Ø(P Ú (Q Ù A)) in 31
33	((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú (Q Ù A))))	replace proposition variable C by Ø((P Ú Q) Ù (P Ú 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) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® D) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® C)))	replace proposition variable B by (Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) in 37
39	((D ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® D) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable C by (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 38
40	(((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú (Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú (Q Ù A)))) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable D by (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú (Q Ù A))) in 39
41	(((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú (Q Ù A)))) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))))	modus ponens with 29, 40
42	((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))	modus ponens with 33, 41
43	((ØP Ú B) ® (P ® B))	replace proposition variable Q by B in 25
44	((ØC Ú B) ® (C ® B))	replace proposition variable P by C in 43
45	((ØC Ú Ø(P Ú ØØ(Q Ù A))) ® (C ® Ø(P Ú ØØ(Q Ù A))))	replace proposition variable B by Ø(P Ú ØØ(Q Ù A)) in 44
46	((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))))	replace proposition variable C by Ø((P Ú Q) Ù (P Ú A)) in 45
47	((D ® (Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A)))) ® (((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® D) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable C by (Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) in 38
48	(((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A)))) ® (((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable D by (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 47
49	(((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A)))))	modus ponens with 46, 48
50	((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú (Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))))	modus ponens with 42, 49
51	(Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A)))	modus ponens with 7, 50
52	(P ® ØØP)	add proposition hilb5
53	(A ® ØØA)	replace proposition variable P by A in 52
54	((P Ú Q) ® ØØ(P Ú Q))	replace proposition variable A by (P Ú Q) in 53
55	((P Ù Q) ® Ø(ØP Ú ØQ))	add proposition defand1
56	(Ø(ØP Ú ØQ) ® (P Ù Q))	add proposition defand2
57	((B ® ØØ(P Ú Q)) ® (ØØØ(P Ú Q) ® ØB))	replace proposition variable A by ØØ(P Ú Q) in 4
58	(((P Ú Q) ® ØØ(P Ú Q)) ® (ØØØ(P Ú Q) ® Ø(P Ú Q)))	replace proposition variable B by (P Ú Q) in 57
59	(ØØØ(P Ú Q) ® Ø(P Ú Q))	modus ponens with 54, 58
60	((D ® C) ® ((Ø(P Ú A) Ú D) ® (Ø(P Ú A) Ú C)))	replace proposition variable B by Ø(P Ú A) in 14
61	((D ® Ø(P Ú Q)) ® ((Ø(P Ú A) Ú D) ® (Ø(P Ú A) Ú Ø(P Ú Q))))	replace proposition variable C by Ø(P Ú Q) in 60
62	((ØØØ(P Ú Q) ® Ø(P Ú Q)) ® ((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® (Ø(P Ú A) Ú Ø(P Ú Q))))	replace proposition variable D by ØØØ(P Ú Q) in 61
63	((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® (Ø(P Ú A) Ú Ø(P Ú Q)))	modus ponens with 59, 62
64	((P Ú Q) ® (Q Ú P))	add axiom axiom3
65	((P Ú B) ® (B Ú P))	replace proposition variable Q by B in 64
66	((C Ú B) ® (B Ú C))	replace proposition variable P by C in 65
67	((C Ú Ø(P Ú Q)) ® (Ø(P Ú Q) Ú C))	replace proposition variable B by Ø(P Ú Q) in 66
68	((Ø(P Ú A) Ú Ø(P Ú Q)) ® (Ø(P Ú Q) Ú Ø(P Ú A)))	replace proposition variable C by Ø(P Ú A) in 67
69	((D ® C) ® (((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® D) ® ((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® C)))	replace proposition variable B by (Ø(P Ú A) Ú ØØØ(P Ú Q)) in 37
70	((D ® (Ø(P Ú Q) Ú Ø(P Ú A))) ® (((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® D) ® ((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® (Ø(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable C by (Ø(P Ú Q) Ú Ø(P Ú A)) in 69
71	(((Ø(P Ú A) Ú Ø(P Ú Q)) ® (Ø(P Ú Q) Ú Ø(P Ú A))) ® (((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® (Ø(P Ú A) Ú Ø(P Ú Q))) ® ((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® (Ø(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable D by (Ø(P Ú A) Ú Ø(P Ú Q)) in 70
72	(((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® (Ø(P Ú A) Ú Ø(P Ú Q))) ® ((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® (Ø(P Ú Q) Ú Ø(P Ú A))))	modus ponens with 68, 71
73	((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® (Ø(P Ú Q) Ú Ø(P Ú A)))	modus ponens with 63, 72
74	((C Ú Ø(P Ú A)) ® (Ø(P Ú A) Ú C))	replace proposition variable B by Ø(P Ú A) in 66
75	((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú A) Ú ØØØ(P Ú Q)))	replace proposition variable C by ØØØ(P Ú Q) in 74
76	((D ® C) ® (((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® D) ® ((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® C)))	replace proposition variable B by (ØØØ(P Ú Q) Ú Ø(P Ú A)) in 37
77	((D ® (Ø(P Ú Q) Ú Ø(P Ú A))) ® (((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® D) ® ((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable C by (Ø(P Ú Q) Ú Ø(P Ú A)) in 76
78	(((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® (Ø(P Ú Q) Ú Ø(P Ú A))) ® (((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú A) Ú ØØØ(P Ú Q))) ® ((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable D by (Ø(P Ú A) Ú ØØØ(P Ú Q)) in 77
79	(((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú A) Ú ØØØ(P Ú Q))) ® ((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú Q) Ú Ø(P Ú A))))	modus ponens with 73, 78
80	((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú Q) Ú Ø(P Ú A)))	modus ponens with 75, 79
81	((C ® (Ø(P Ú Q) Ú Ø(P Ú A))) ® (Ø(Ø(P Ú Q) Ú Ø(P Ú A)) ® ØC))	replace proposition variable B by (Ø(P Ú Q) Ú Ø(P Ú A)) in 20
82	(((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú Q) Ú Ø(P Ú A))) ® (Ø(Ø(P Ú Q) Ú Ø(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))))	replace proposition variable C by (ØØØ(P Ú Q) Ú Ø(P Ú A)) in 81
83	(Ø(Ø(P Ú Q) Ú Ø(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)))	modus ponens with 80, 82
84	((P Ù B) ® Ø(ØP Ú ØB))	replace proposition variable Q by B in 55
85	((C Ù B) ® Ø(ØC Ú ØB))	replace proposition variable P by C in 84
86	((C Ù (P Ú A)) ® Ø(ØC Ú Ø(P Ú A)))	replace proposition variable B by (P Ú A) in 85
87	(((P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A)))	replace proposition variable C by (P Ú Q) in 86
88	((D ® C) ® ((((P Ú Q) Ù (P Ú A)) ® D) ® (((P Ú Q) Ù (P Ú A)) ® C)))	replace proposition variable B by ((P Ú Q) Ù (P Ú A)) in 37
89	((D ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® ((((P Ú Q) Ù (P Ú A)) ® D) ® (((P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable C by Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) in 88
90	((Ø(Ø(P Ú Q) Ú Ø(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® ((((P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))) ® (((P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)))))	replace proposition variable D by Ø(Ø(P Ú Q) Ú Ø(P Ú A)) in 89
91	((((P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))) ® (((P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))))	modus ponens with 83, 90
92	(((P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)))	modus ponens with 87, 91
93	(Ø(ØP Ú ØB) ® (P Ù B))	replace proposition variable Q by B in 56
94	(Ø(ØC Ú ØB) ® (C Ù B))	replace proposition variable P by C in 93
95	(Ø(ØC Ú Ø(P Ú A)) ® (C Ù (P Ú A)))	replace proposition variable B by (P Ú A) in 94
96	(Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A)))	replace proposition variable C by ØØ(P Ú Q) in 95
97	((D ® (ØØ(P Ú Q) Ù (P Ú A))) ® ((((P Ú Q) Ù (P Ú A)) ® D) ® (((P Ú Q) Ù (P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A)))))	replace proposition variable C by (ØØ(P Ú Q) Ù (P Ú A)) in 88
98	((Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A))) ® ((((P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((P Ú Q) Ù (P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A)))))	replace proposition variable D by Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) in 97
99	((((P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((P Ú Q) Ù (P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A))))	modus ponens with 96, 98
100	(((P Ú Q) Ù (P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A)))	modus ponens with 92, 99
101	((C ® (ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® ØC))	replace proposition variable B by (ØØ(P Ú Q) Ù (P Ú A)) in 20
102	((((P Ú Q) Ù (P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø((P Ú Q) Ù (P Ú A))))	replace proposition variable C by ((P Ú Q) Ù (P Ú A)) in 101
103	(Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø((P Ú Q) Ù (P Ú A)))	modus ponens with 100, 102
104	((C ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ((P Ú Q) Ù (P Ú A)) ® ØC))	replace proposition variable B by Ø((P Ú Q) Ù (P Ú A)) in 20
105	((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ((P Ú Q) Ù (P Ú A)) ® ØØ(ØØ(P Ú Q) Ù (P Ú A))))	replace proposition variable C by Ø(ØØ(P Ú Q) Ù (P Ú A)) in 104
106	(ØØ((P Ú Q) Ù (P Ú A)) ® ØØ(ØØ(P Ú Q) Ù (P Ú A)))	modus ponens with 103, 105
107	((D ® C) ® ((Ø(P Ú ØØ(Q Ù A)) Ú D) ® (Ø(P Ú ØØ(Q Ù A)) Ú C)))	replace proposition variable B by Ø(P Ú ØØ(Q Ù A)) in 14
108	((D ® ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® ((Ø(P Ú ØØ(Q Ù A)) Ú D) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A)))))	replace proposition variable C by ØØ(ØØ(P Ú Q) Ù (P Ú A)) in 107
109	((ØØ((P Ú Q) Ù (P Ú A)) ® ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® ((Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A)))))	replace proposition variable D by ØØ((P Ú Q) Ù (P Ú A)) in 108
110	((Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))))	modus ponens with 106, 109
111	((C Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú C))	replace proposition variable B by ØØ(ØØ(P Ú Q) Ù (P Ú A)) in 66
112	((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))	replace proposition variable C by Ø(P Ú ØØ(Q Ù A)) in 111
113	((D ® C) ® (((Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) ® C)))	replace proposition variable B by (Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) in 37
114	((D ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable C by (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 113
115	(((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable D by (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) in 114
116	(((Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))))	modus ponens with 112, 115
117	((Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))	modus ponens with 110, 116
118	((C Ú Ø(P Ú ØØ(Q Ù A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú C))	replace proposition variable B by Ø(P Ú ØØ(Q Ù A)) in 66
119	((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))))	replace proposition variable C by ØØ((P Ú Q) Ù (P Ú A)) in 118
120	((D ® C) ® (((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® D) ® ((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® C)))	replace proposition variable B by (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 37
121	((D ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® D) ® ((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable C by (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 120
122	(((Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A)))) ® ((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable D by (Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A))) in 121
123	(((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ((P Ú Q) Ù (P Ú A)))) ® ((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))))	modus ponens with 117, 122
124	((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))	modus ponens with 119, 123
125	((C ® Ø(P Ú ØØ(Q Ù A))) ® (ØC Ú Ø(P Ú ØØ(Q Ù A))))	replace proposition variable B by Ø(P Ú ØØ(Q Ù A)) in 31
126	((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))	replace proposition variable C by Ø((P Ú Q) Ù (P Ú A)) in 125
127	((D ® C) ® (((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® D) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® C)))	replace proposition variable B by (Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) in 37
128	((D ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® D) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable C by (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 127
129	(((ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable D by (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 128
130	(((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ((P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))))	modus ponens with 124, 129
131	((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))	modus ponens with 126, 130
132	((ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))))	replace proposition variable C by Ø(ØØ(P Ú Q) Ù (P Ú A)) in 45
133	((D ® (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A)))) ® (((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® D) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable C by (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) in 127
134	(((ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A)))) ® (((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable D by (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 133
135	(((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A)))))	modus ponens with 132, 134
136	((Ø((P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))))	modus ponens with 131, 135
137	(Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A)))	modus ponens with 51, 136
138	(B ® ØØB)	replace proposition variable P by B in 52
139	((P Ú A) ® ØØ(P Ú A))	replace proposition variable B by (P Ú A) in 138
140	((C ® ØØ(P Ú A)) ® (ØØØ(P Ú A) ® ØC))	replace proposition variable B by ØØ(P Ú A) in 20
141	(((P Ú A) ® ØØ(P Ú A)) ® (ØØØ(P Ú A) ® Ø(P Ú A)))	replace proposition variable C by (P Ú A) in 140
142	(ØØØ(P Ú A) ® Ø(P Ú A))	modus ponens with 139, 141
143	((D ® C) ® ((ØØØ(P Ú Q) Ú D) ® (ØØØ(P Ú Q) Ú C)))	replace proposition variable B by ØØØ(P Ú Q) in 14
144	((D ® Ø(P Ú A)) ® ((ØØØ(P Ú Q) Ú D) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))))	replace proposition variable C by Ø(P Ú A) in 143
145	((ØØØ(P Ú A) ® Ø(P Ú A)) ® ((ØØØ(P Ú Q) Ú ØØØ(P Ú A)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))))	replace proposition variable D by ØØØ(P Ú A) in 144
146	((ØØØ(P Ú Q) Ú ØØØ(P Ú A)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A)))	modus ponens with 142, 145
147	((C ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® ØC))	replace proposition variable B by (ØØØ(P Ú Q) Ú Ø(P Ú A)) in 20
148	(((ØØØ(P Ú Q) Ú ØØØ(P Ú A)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A))))	replace proposition variable C by (ØØØ(P Ú Q) Ú ØØØ(P Ú A)) in 147
149	(Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)))	modus ponens with 146, 148
150	((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)))	replace proposition variable C by ØØ(P Ú Q) in 86
151	((D ® C) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® C)))	replace proposition variable B by (ØØ(P Ú Q) Ù (P Ú A)) in 37
152	((D ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A))) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)))))	replace proposition variable C by Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) in 151
153	((Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A))) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)))))	replace proposition variable D by Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) in 152
154	(((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A))))	modus ponens with 149, 153
155	((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)))	modus ponens with 150, 154
156	(Ø(ØC Ú ØØØ(P Ú A)) ® (C Ù ØØ(P Ú A)))	replace proposition variable B by ØØ(P Ú A) in 94
157	(Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) ® (ØØ(P Ú Q) Ù ØØ(P Ú A)))	replace proposition variable C by ØØ(P Ú Q) in 156
158	((D ® (ØØ(P Ú Q) Ù ØØ(P Ú A))) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® (ØØ(P Ú Q) Ù ØØ(P Ú A)))))	replace proposition variable C by (ØØ(P Ú Q) Ù ØØ(P Ú A)) in 151
159	((Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) ® (ØØ(P Ú Q) Ù ØØ(P Ú A))) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A))) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® (ØØ(P Ú Q) Ù ØØ(P Ú A)))))	replace proposition variable D by Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) in 158
160	(((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A))) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® (ØØ(P Ú Q) Ù ØØ(P Ú A))))	modus ponens with 157, 159
161	((ØØ(P Ú Q) Ù (P Ú A)) ® (ØØ(P Ú Q) Ù ØØ(P Ú A)))	modus ponens with 155, 160
162	((C ® (ØØ(P Ú Q) Ù ØØ(P Ú A))) ® (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® ØC))	replace proposition variable B by (ØØ(P Ú Q) Ù ØØ(P Ú A)) in 20
163	(((ØØ(P Ú Q) Ù (P Ú A)) ® (ØØ(P Ú Q) Ù ØØ(P Ú A))) ® (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))))	replace proposition variable C by (ØØ(P Ú Q) Ù (P Ú A)) in 162
164	(Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A)))	modus ponens with 161, 163
165	((C ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) ® ØC))	replace proposition variable B by Ø(ØØ(P Ú Q) Ù (P Ú A)) in 20
166	((Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) ® ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A))))	replace proposition variable C by Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) in 165
167	(ØØ(ØØ(P Ú Q) Ù (P Ú A)) ® ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)))	modus ponens with 164, 166
168	((D ® ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® ((Ø(P Ú ØØ(Q Ù A)) Ú D) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)))))	replace proposition variable C by ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) in 107
169	((ØØ(ØØ(P Ú Q) Ù (P Ú A)) ® ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® ((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)))))	replace proposition variable D by ØØ(ØØ(P Ú Q) Ù (P Ú A)) in 168
170	((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A))))	modus ponens with 167, 169
171	((C Ú ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú C))	replace proposition variable B by ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) in 66
172	((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))	replace proposition variable C by Ø(P Ú ØØ(Q Ù A)) in 171
173	((D ® C) ® (((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® C)))	replace proposition variable B by (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) in 37
174	((D ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable C by (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 173
175	(((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable D by (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A))) in 174
176	(((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))))	modus ponens with 172, 175
177	((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))	modus ponens with 170, 176
178	((ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))))	replace proposition variable C by ØØ(ØØ(P Ú Q) Ù (P Ú A)) in 118
179	((D ® C) ® (((ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® D) ® ((ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® C)))	replace proposition variable B by (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 37
180	((D ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® D) ® ((ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable C by (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 179
181	(((Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A)))) ® ((ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable D by (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A))) in 180
182	(((ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (Ø(P Ú ØØ(Q Ù A)) Ú ØØ(ØØ(P Ú Q) Ù (P Ú A)))) ® ((ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))))	modus ponens with 177, 181
183	((ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))	modus ponens with 178, 182
184	((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))	replace proposition variable C by Ø(ØØ(P Ú Q) Ù (P Ú A)) in 125
185	((D ® C) ® (((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® D) ® ((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® C)))	replace proposition variable B by (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) in 37
186	((D ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® D) ® ((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable C by (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 185
187	(((ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® (((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® ((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable D by (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 186
188	(((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù (P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® ((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))))	modus ponens with 183, 187
189	((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))))	modus ponens with 184, 188
190	((ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(P Ú ØØ(Q Ù A))))	replace proposition variable C by Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) in 45
191	((D ® (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(P Ú ØØ(Q Ù A)))) ® (((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® D) ® ((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable C by (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) in 185
192	(((ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) ® (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(P Ú ØØ(Q Ù A)))) ® (((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® ((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(P Ú ØØ(Q Ù A))))))	replace proposition variable D by (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A))) in 191
193	(((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (ØØ(ØØ(P Ú Q) Ù ØØ(P Ú A)) Ú Ø(P Ú ØØ(Q Ù A)))) ® ((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(P Ú ØØ(Q Ù A)))))	modus ponens with 190, 192
194	((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) ® (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(P Ú ØØ(Q Ù A))))	modus ponens with 189, 193
195	(Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(P Ú ØØ(Q Ù A)))	modus ponens with 137, 194
196	(Ø(ØØ(P Ú Q) Ù ØØ(P Ú B)) ® Ø(P Ú ØØ(Q Ù B)))	replace proposition variable A by B in 195
197	(Ø(ØØ(P Ú C) Ù ØØ(P Ú B)) ® Ø(P Ú ØØ(C Ù B)))	replace proposition variable Q by C in 196
198	(Ø(ØØ(D Ú C) Ù ØØ(D Ú B)) ® Ø(D Ú ØØ(C Ù B)))	replace proposition variable P by D in 197
199	(Ø(ØØ(D Ú C) Ù ØØ(D Ú ØA)) ® Ø(D Ú ØØ(C Ù ØA)))	replace proposition variable B by ØA in 198
200	(Ø(ØØ(D Ú ØQ) Ù ØØ(D Ú ØA)) ® Ø(D Ú ØØ(ØQ Ù ØA)))	replace proposition variable C by ØQ in 199
201	(Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) ® Ø(ØP Ú ØØ(ØQ Ù ØA)))	replace proposition variable D by ØP in 200
202	(Ø(Ø(P Ù Q) Ù ØØ(ØP Ú ØA)) ® Ø(ØP Ú ØØ(ØQ Ù ØA)))	reverse abbreviation and in 201 at occurence 1
203	(Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA)))	reverse abbreviation and in 202 at occurence 1
204	(Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA)))	reverse abbreviation and in 203 at occurence 1
205	((P Ú Q) ® Ø(ØP Ù ØQ))	add proposition hilb38
206	((P Ú B) ® Ø(ØP Ù ØB))	replace proposition variable Q by B in 205
207	((C Ú B) ® Ø(ØC Ù ØB))	replace proposition variable P by C in 206
208	((C Ú (P Ù A)) ® Ø(ØC Ù Ø(P Ù A)))	replace proposition variable B by (P Ù A) in 207
209	(((P Ù Q) Ú (P Ù A)) ® Ø(Ø(P Ù Q) Ù Ø(P Ù A)))	replace proposition variable C by (P Ù Q) in 208
210	((C ® Ø(Ø(P Ù Q) Ù Ø(P Ù A))) ® (ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) ® ØC))	replace proposition variable B by Ø(Ø(P Ù Q) Ù Ø(P Ù A)) in 20
211	((((P Ù Q) Ú (P Ù A)) ® Ø(Ø(P Ù Q) Ù Ø(P Ù A))) ® (ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) ® Ø((P Ù Q) Ú (P Ù A))))	replace proposition variable C by ((P Ù Q) Ú (P Ù A)) in 210
212	(ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) ® Ø((P Ù Q) Ú (P Ù A)))	modus ponens with 209, 211
213	((D ® C) ® (((P Ù Ø(ØQ Ù ØA)) Ú D) ® ((P Ù Ø(ØQ Ù ØA)) Ú C)))	replace proposition variable B by (P Ù Ø(ØQ Ù ØA)) in 14
214	((D ® Ø((P Ù Q) Ú (P Ù A))) ® (((P Ù Ø(ØQ Ù ØA)) Ú D) ® ((P Ù Ø(ØQ Ù ØA)) Ú Ø((P Ù Q) Ú (P Ù A)))))	replace proposition variable C by Ø((P Ù Q) Ú (P Ù A)) in 213
215	((ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) ® Ø((P Ù Q) Ú (P Ù A))) ® (((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) ® ((P Ù Ø(ØQ Ù ØA)) Ú Ø((P Ù Q) Ú (P Ù A)))))	replace proposition variable D by ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) in 214
216	(((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) ® ((P Ù Ø(ØQ Ù ØA)) Ú Ø((P Ù Q) Ú (P Ù A))))	modus ponens with 212, 215
217	((C Ú Ø((P Ù Q) Ú (P Ù A))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú C))	replace proposition variable B by Ø((P Ù Q) Ú (P Ù A)) in 66
218	(((P Ù Ø(ØQ Ù ØA)) Ú Ø((P Ù Q) Ú (P Ù A))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))))	replace proposition variable C by (P Ù Ø(ØQ Ù ØA)) in 217
219	((D ® C) ® ((((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) ® D) ® (((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) ® C)))	replace proposition variable B by ((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) in 37
220	((D ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))) ® ((((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) ® D) ® (((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))))))	replace proposition variable C by (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) in 219
221	((((P Ù Ø(ØQ Ù ØA)) Ú Ø((P Ù Q) Ú (P Ù A))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))) ® ((((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) ® ((P Ù Ø(ØQ Ù ØA)) Ú Ø((P Ù Q) Ú (P Ù A)))) ® (((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))))))	replace proposition variable D by ((P Ù Ø(ØQ Ù ØA)) Ú Ø((P Ù Q) Ú (P Ù A))) in 220
222	((((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) ® ((P Ù Ø(ØQ Ù ØA)) Ú Ø((P Ù Q) Ú (P Ù A)))) ® (((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))))	modus ponens with 218, 221
223	(((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))))	modus ponens with 216, 222
224	((C Ú (P Ù Ø(ØQ Ù ØA))) ® ((P Ù Ø(ØQ Ù ØA)) Ú C))	replace proposition variable B by (P Ù Ø(ØQ Ù ØA)) in 66
225	((ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® ((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))))	replace proposition variable C by ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) in 224
226	((D ® C) ® (((ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® D) ® ((ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® C)))	replace proposition variable B by (ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) in 37
227	((D ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))) ® (((ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® D) ® ((ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))))))	replace proposition variable C by (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) in 226
228	((((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))) ® (((ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® ((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A)))) ® ((ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))))))	replace proposition variable D by ((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A))) in 227
229	(((ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® ((P Ù Ø(ØQ Ù ØA)) Ú ØØ(Ø(P Ù Q) Ù Ø(P Ù A)))) ® ((ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))))	modus ponens with 223, 228
230	((ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))))	modus ponens with 225, 229
231	((C ® (P Ù Ø(ØQ Ù ØA))) ® (ØC Ú (P Ù Ø(ØQ Ù ØA))))	replace proposition variable B by (P Ù Ø(ØQ Ù ØA)) in 31
232	((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))))	replace proposition variable C by Ø(Ø(P Ù Q) Ù Ø(P Ù A)) in 231
233	((D ® C) ® (((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® D) ® ((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® C)))	replace proposition variable B by (Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) in 37
234	((D ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))) ® (((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® D) ® ((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))))))	replace proposition variable C by (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) in 233
235	(((ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))) ® (((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))) ® ((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))))))	replace proposition variable D by (ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) in 234
236	(((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (ØØ(Ø(P Ù Q) Ù Ø(P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))) ® ((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))))	modus ponens with 230, 235
237	((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))))	modus ponens with 232, 236
238	((ØC Ú (P Ù Ø(ØQ Ù ØA))) ® (C ® (P Ù Ø(ØQ Ù ØA))))	replace proposition variable B by (P Ù Ø(ØQ Ù ØA)) in 44
239	((Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® (((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))))	replace proposition variable C by ((P Ù Q) Ú (P Ù A)) in 238
240	((D ® (((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA)))) ® (((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® D) ® ((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))))))	replace proposition variable C by (((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) in 233
241	(((Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® (((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA)))) ® (((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))) ® ((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))))))	replace proposition variable D by (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) in 240
242	(((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))) ® ((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA)))))	modus ponens with 239, 241
243	((Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))))	modus ponens with 237, 242
244	(((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA)))	modus ponens with 204, 243
245	(Ø(ØP Ù ØQ) ® (P Ú Q))	add proposition hilb39
246	(Ø(ØP Ù ØB) ® (P Ú B))	replace proposition variable Q by B in 245
247	(Ø(ØC Ù ØB) ® (C Ú B))	replace proposition variable P by C in 246
248	(Ø(ØC Ù ØA) ® (C Ú A))	replace proposition variable B by A in 247
249	(Ø(ØQ Ù ØA) ® (Q Ú A))	replace proposition variable C by Q in 248
250	((C ® (Q Ú A)) ® (Ø(Q Ú A) ® ØC))	replace proposition variable B by (Q Ú A) in 20
251	((Ø(ØQ Ù ØA) ® (Q Ú A)) ® (Ø(Q Ú A) ® ØØ(ØQ Ù ØA)))	replace proposition variable C by Ø(ØQ Ù ØA) in 250
252	(Ø(Q Ú A) ® ØØ(ØQ Ù ØA))	modus ponens with 249, 251
253	((D ® C) ® ((ØP Ú D) ® (ØP Ú C)))	replace proposition variable B by ØP in 14
254	((D ® ØØ(ØQ Ù ØA)) ® ((ØP Ú D) ® (ØP Ú ØØ(ØQ Ù ØA))))	replace proposition variable C by ØØ(ØQ Ù ØA) in 253
255	((Ø(Q Ú A) ® ØØ(ØQ Ù ØA)) ® ((ØP Ú Ø(Q Ú A)) ® (ØP Ú ØØ(ØQ Ù ØA))))	replace proposition variable D by Ø(Q Ú A) in 254
256	((ØP Ú Ø(Q Ú A)) ® (ØP Ú ØØ(ØQ Ù ØA)))	modus ponens with 252, 255
257	((C ® (ØP Ú ØØ(ØQ Ù ØA))) ® (Ø(ØP Ú ØØ(ØQ Ù ØA)) ® ØC))	replace proposition variable B by (ØP Ú ØØ(ØQ Ù ØA)) in 20
258	(((ØP Ú Ø(Q Ú A)) ® (ØP Ú ØØ(ØQ Ù ØA))) ® (Ø(ØP Ú ØØ(ØQ Ù ØA)) ® Ø(ØP Ú Ø(Q Ú A))))	replace proposition variable C by (ØP Ú Ø(Q Ú A)) in 257
259	(Ø(ØP Ú ØØ(ØQ Ù ØA)) ® Ø(ØP Ú Ø(Q Ú A)))	modus ponens with 256, 258
260	((C Ù Ø(ØQ Ù ØA)) ® Ø(ØC Ú ØØ(ØQ Ù ØA)))	replace proposition variable B by Ø(ØQ Ù ØA) in 85
261	((P Ù Ø(ØQ Ù ØA)) ® Ø(ØP Ú ØØ(ØQ Ù ØA)))	replace proposition variable C by P in 260
262	((D ® C) ® (((P Ù Ø(ØQ Ù ØA)) ® D) ® ((P Ù Ø(ØQ Ù ØA)) ® C)))	replace proposition variable B by (P Ù Ø(ØQ Ù ØA)) in 37
263	((D ® Ø(ØP Ú Ø(Q Ú A))) ® (((P Ù Ø(ØQ Ù ØA)) ® D) ® ((P Ù Ø(ØQ Ù ØA)) ® Ø(ØP Ú Ø(Q Ú A)))))	replace proposition variable C by Ø(ØP Ú Ø(Q Ú A)) in 262
264	((Ø(Ø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 263
265	(((P Ù Ø(ØQ Ù ØA)) ® Ø(ØP Ú ØØ(ØQ Ù ØA))) ® ((P Ù Ø(ØQ Ù ØA)) ® Ø(ØP Ú Ø(Q Ú A))))	modus ponens with 259, 264
266	((P Ù Ø(ØQ Ù ØA)) ® Ø(ØP Ú Ø(Q Ú A)))	modus ponens with 261, 265
267	(Ø(ØC Ú Ø(Q Ú A)) ® (C Ù (Q Ú A)))	replace proposition variable B by (Q Ú A) in 94
268	(Ø(ØP Ú Ø(Q Ú A)) ® (P Ù (Q Ú A)))	replace proposition variable C by P in 267
269	((D ® (P Ù (Q Ú A))) ® (((P Ù Ø(ØQ Ù ØA)) ® D) ® ((P Ù Ø(ØQ Ù ØA)) ® (P Ù (Q Ú A)))))	replace proposition variable C by (P Ù (Q Ú A)) in 262
270	((Ø(Ø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 269
271	(((P Ù Ø(ØQ Ù ØA)) ® Ø(ØP Ú Ø(Q Ú A))) ® ((P Ù Ø(ØQ Ù ØA)) ® (P Ù (Q Ú A))))	modus ponens with 268, 270
272	((P Ù Ø(ØQ Ù ØA)) ® (P Ù (Q Ú A)))	modus ponens with 266, 271
273	((D ® C) ® ((Ø((P Ù Q) Ú (P Ù A)) Ú D) ® (Ø((P Ù Q) Ú (P Ù A)) Ú C)))	replace proposition variable B by Ø((P Ù Q) Ú (P Ù A)) in 14
274	((D ® (P Ù (Q Ú A))) ® ((Ø((P Ù Q) Ú (P Ù A)) Ú D) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A)))))	replace proposition variable C by (P Ù (Q Ú A)) in 273
275	(((P Ù Ø(ØQ Ù ØA)) ® (P Ù (Q Ú A))) ® ((Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A)))))	replace proposition variable D by (P Ù Ø(ØQ Ù ØA)) in 274
276	((Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A))))	modus ponens with 272, 275
277	((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))))	replace proposition variable C by ((P Ù Q) Ú (P Ù A)) in 231
278	((D ® C) ® (((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® D) ® ((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® C)))	replace proposition variable B by (((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) in 37
279	((D ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A)))) ® (((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® D) ® ((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A))))))	replace proposition variable C by (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A))) in 278
280	(((Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A)))) ® (((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))) ® ((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A))))))	replace proposition variable D by (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA))) in 279
281	(((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù Ø(ØQ Ù ØA)))) ® ((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A)))))	modus ponens with 276, 280
282	((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A))))	modus ponens with 277, 281
283	((ØC Ú (P Ù (Q Ú A))) ® (C ® (P Ù (Q Ú A))))	replace proposition variable B by (P Ù (Q Ú A)) in 44
284	((Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A))) ® (((P Ù Q) Ú (P Ù A)) ® (P Ù (Q Ú A))))	replace proposition variable C by ((P Ù Q) Ú (P Ù A)) in 283
285	((D ® (((P Ù Q) Ú (P Ù A)) ® (P Ù (Q Ú A)))) ® (((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® D) ® ((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (((P Ù Q) Ú (P Ù A)) ® (P Ù (Q Ú A))))))	replace proposition variable C by (((P Ù Q) Ú (P Ù A)) ® (P Ù (Q Ú A))) in 278
286	(((Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A))) ® (((P Ù Q) Ú (P Ù A)) ® (P Ù (Q Ú A)))) ® (((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A)))) ® ((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (((P Ù Q) Ú (P Ù A)) ® (P Ù (Q Ú A))))))	replace proposition variable D by (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A))) in 285
287	(((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø((P Ù Q) Ú (P Ù A)) Ú (P Ù (Q Ú A)))) ® ((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (((P Ù Q) Ú (P Ù A)) ® (P Ù (Q Ú A)))))	modus ponens with 284, 286
288	((((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) ® (((P Ù Q) Ú (P Ù A)) ® (P Ù (Q Ú A))))	modus ponens with 282, 287
289	(((P Ù Q) Ú (P Ù A)) ® (P Ù (Q Ú A)))	modus ponens with 244, 288
	qed

Cross References

This document is used by the following documents:

predtheo2_1.00.00_1.02.00.o.html