First distributive law (first direction):
1. Proposition
((P Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A))) (hilb36)
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)
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 Ú A) ® ((P Ú Q) ® ((P Ú P) Ú (Q Ù A)))) | elementary equivalence in 35 at 1 of hilb14 with hilb15 |
37 | ((P Ú A) ® ((P Ú Q) ® (P Ú (Q Ù A)))) | elementary equivalence in 36 at 1 of hilb11 with hilb12 |
38 | ((D ® ((P Ú Q) ® (P Ú (Q Ù A)))) ® ((P Ú Q) ® (D ® (P Ú (Q Ù A))))) | replace proposition variable C by (P Ú Q) in 25 |
39 | (((P Ú A) ® ((P Ú Q) ® (P Ú (Q Ù A)))) ® ((P Ú Q) ® ((P Ú A) ® (P Ú (Q Ù A))))) | replace proposition variable D by (P Ú A) in 38 |
40 | ((P Ú Q) ® ((P Ú A) ® (P Ú (Q Ù A)))) | modus ponens with 37, 39 |
41 | ((P ® (Q ® A)) ® ((P Ù Q) ® A)) | add proposition hilb29 |
42 | ((P ® (Q ® B)) ® ((P Ù Q) ® B)) | replace proposition variable A by B in 41 |
43 | ((P ® (C ® B)) ® ((P Ù C) ® B)) | replace proposition variable Q by C in 42 |
44 | ((D ® (C ® B)) ® ((D Ù C) ® B)) | replace proposition variable P by D in 43 |
45 | ((D ® (C ® (P Ú (Q Ù A)))) ® ((D Ù C) ® (P Ú (Q Ù A)))) | replace proposition variable B by (P Ú (Q Ù A)) in 44 |
46 | ((D ® ((P Ú A) ® (P Ú (Q Ù A)))) ® ((D Ù (P Ú A)) ® (P Ú (Q Ù A)))) | replace proposition variable C by (P Ú A) in 45 |
47 | (((P Ú Q) ® ((P Ú A) ® (P Ú (Q Ù A)))) ® (((P Ú Q) Ù (P Ú A)) ® (P Ú (Q Ù A)))) | replace proposition variable D by (P Ú Q) in 46 |
48 | (((P Ú Q) Ù (P Ú A)) ® (P Ú (Q Ù A))) | modus ponens with 40, 47 |
qed |
A form for the abbreviation rule form for disjunction (first direction):
3. Proposition
((P Ú Q) ® Ø(ØP Ù ØQ)) (hilb38)
1 | (P ® P) | add proposition hilb2 |
2 | (Q ® Q) | replace proposition variable P by Q in 1 |
3 | ((P Ú Q) ® (P Ú Q)) | replace proposition variable Q by (P Ú Q) in 2 |
4 | ((P Ú Q) ® ØØ(P Ú Q)) | elementary equivalence in 3 at 5 of hilb5 with hilb6 |
5 | ((P Ú Q) ® ØØ(ØØP Ú Q)) | elementary equivalence in 4 at 8 of hilb5 with hilb6 |
6 | ((P Ú Q) ® ØØ(ØØP Ú ØØQ)) | elementary equivalence in 5 at 11 of hilb5 with hilb6 |
7 | ((P Ú Q) ® Ø(ØP Ù ØQ)) | reverse abbreviation and in 6 at occurence 1 |
qed |
A form for the abbreviation rule form for disjunction (second direction):
4. Proposition
(Ø(ØP Ù ØQ) ® (P Ú Q)) (hilb39)
1 | (P ® P) | add proposition hilb2 |
2 | (Q ® Q) | replace proposition variable P by Q in 1 |
3 | ((P Ú Q) ® (P Ú Q)) | replace proposition variable Q by (P Ú Q) in 2 |
4 | (ØØ(P Ú Q) ® (P Ú Q)) | elementary equivalence in 3 at 2 of hilb5 with hilb6 |
5 | (ØØ(ØØP Ú Q) ® (P Ú Q)) | elementary equivalence in 4 at 5 of hilb5 with hilb6 |
6 | (ØØ(ØØP Ú ØØQ) ® (P Ú Q)) | elementary equivalence in 5 at 8 of hilb5 with hilb6 |
7 | (Ø(ØP Ù ØQ) ® (P Ú Q)) | reverse abbreviation and in 6 at occurence 1 |
qed |
By duality we get the second distributive law (first direction):
5. Proposition
((P Ù (Q Ú A)) ® ((P Ù Q) Ú (P Ù A))) (hilb40)
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 Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) | elementary equivalence in 7 at 5 of hilb5 with hilb6 |
9 | (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) | elementary equivalence in 8 at 12 of hilb5 with hilb6 |
10 | (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) | elementary equivalence in 9 at 17 of hilb5 with hilb6 |
11 | (Ø(P Ú ØØ(Q Ù B)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú B))) | replace proposition variable A by B in 10 |
12 | (Ø(P Ú ØØ(C Ù B)) ® Ø(ØØ(P Ú C) Ù ØØ(P Ú B))) | replace proposition variable Q by C in 11 |
13 | (Ø(D Ú ØØ(C Ù B)) ® Ø(ØØ(D Ú C) Ù ØØ(D Ú B))) | replace proposition variable P by D in 12 |
14 | (Ø(D Ú ØØ(C Ù ØA)) ® Ø(ØØ(D Ú C) Ù ØØ(D Ú ØA))) | replace proposition variable B by ØA in 13 |
15 | (Ø(D Ú ØØ(ØQ Ù ØA)) ® Ø(ØØ(D Ú ØQ) Ù ØØ(D Ú ØA))) | replace proposition variable C by ØQ in 14 |
16 | (Ø(ØP Ú ØØ(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) | replace proposition variable D by ØP in 15 |
17 | ((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) | reverse abbreviation and in 16 at occurence 1 |
18 | ((P Ù (Q Ú A)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) | elementary equivalence in 17 at 1 of hilb39 with hilb38 |
19 | ((P Ù (Q Ú A)) ® (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))) | elementary equivalence in 18 at 1 of hilb39 with hilb38 |
20 | ((P Ù (Q Ú A)) ® ((P Ù Q) Ú Ø(ØP Ú ØA))) | reverse abbreviation and in 19 at occurence 1 |
21 | ((P Ù (Q Ú A)) ® ((P Ù Q) Ú (P Ù A))) | reverse abbreviation and in 20 at occurence 1 |
qed |
The second distributive law (second direction):
6. Proposition
(((P Ù Q) Ú (P Ù A)) ® (P Ù (Q Ú A))) (hilb41)
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 Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) | elementary equivalence in 7 at 13 of hilb5 with hilb6 |
9 | (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) | elementary equivalence in 8 at 4 of hilb5 with hilb6 |
10 | (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(P Ú ØØ(Q Ù A))) | elementary equivalence in 9 at 9 of hilb5 with hilb6 |
11 | (Ø(ØØ(P Ú Q) Ù ØØ(P Ú B)) ® Ø(P Ú ØØ(Q Ù B))) | replace proposition variable A by B in 10 |
12 | (Ø(ØØ(P Ú C) Ù ØØ(P Ú B)) ® Ø(P Ú ØØ(C Ù B))) | replace proposition variable Q by C in 11 |
13 | (Ø(ØØ(D Ú C) Ù ØØ(D Ú B)) ® Ø(D Ú ØØ(C Ù B))) | replace proposition variable P by D in 12 |
14 | (Ø(ØØ(D Ú C) Ù ØØ(D Ú ØA)) ® Ø(D Ú ØØ(C Ù ØA))) | replace proposition variable B by ØA in 13 |
15 | (Ø(ØØ(D Ú ØQ) Ù ØØ(D Ú ØA)) ® Ø(D Ú ØØ(ØQ Ù ØA))) | replace proposition variable C by ØQ in 14 |
16 | (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) ® Ø(ØP Ú ØØ(ØQ Ù ØA))) | replace proposition variable D by ØP in 15 |
17 | (Ø(Ø(P Ù Q) Ù ØØ(ØP Ú ØA)) ® Ø(ØP Ú ØØ(ØQ Ù ØA))) | reverse abbreviation and in 16 at occurence 1 |
18 | (Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA))) | reverse abbreviation and in 17 at occurence 1 |
19 | (Ø(Ø(P Ù Q) Ù Ø(P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) | reverse abbreviation and in 18 at occurence 1 |
20 | (((P Ù Q) Ú (P Ù A)) ® (P Ù Ø(ØQ Ù ØA))) | elementary equivalence in 19 at 1 of hilb39 with hilb38 |
21 | (((P Ù Q) Ú (P Ù A)) ® (P Ù (Q Ú A))) | elementary equivalence in 20 at 1 of hilb39 with hilb38 |
qed |