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 |