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:

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