for questions or link request: module admin

Further Theorems of Propositional Calculus

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

Description

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

References

This document uses the results of the following documents:

Content

Negation of a conjunction:

1. Proposition
      ¬(P ∧ Q) → (¬P ∨ ¬Q)     (hilb18)

Proof:
1 ¬¬P → P add proposition hilb6
2 ¬¬Q → Q replace proposition variable P by Q in 1
3 ¬¬(¬P ∨ ¬Q) → (¬P ∨ ¬Q) replace proposition variable Q by ¬P ∨ ¬Q in 2
4 ¬(P ∧ Q) → (¬P ∨ ¬Q) reverse abbreviation and in 3 at occurence 1
qed

The reverse of a negation of a conjunction:

2. Proposition
      (¬P ∨ ¬Q) → ¬(P ∧ Q)     (hilb19)

Proof:
1 P → ¬¬P add proposition hilb5
2 Q → ¬¬Q replace proposition variable P by Q in 1
3 (¬P ∨ ¬Q) → ¬¬(¬P ∨ ¬Q) replace proposition variable Q by ¬P ∨ ¬Q in 2
4 (¬P ∨ ¬Q) → ¬(P ∧ Q) reverse abbreviation and in 3 at occurence 1
qed

Negation of a disjunction:

3. Proposition
      ¬(P ∨ Q) → (¬P ∧ ¬Q)     (hilb20)

Proof:
1 ¬¬P → P add proposition hilb6
2 ¬¬Q → Q replace proposition variable P by Q in 1
3 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
4 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 3
5 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 4
6 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 5
7 (D → C) → ((Q ∨ D) → (Q ∨ C)) replace proposition variable B by Q in 6
8 (D → P) → ((Q ∨ D) → (Q ∨ P)) replace proposition variable C by P in 7
9 (¬¬P → P) → ((Q ∨ ¬¬P) → (Q ∨ P)) replace proposition variable D by ¬¬P in 8
10 (Q ∨ ¬¬P) → (Q ∨ P) modus ponens with 1, 9
11 (P ∨ Q) → (Q ∨ P) add axiom axiom3
12 (P ∨ A) → (A ∨ P) replace proposition variable Q by A in 11
13 (B ∨ A) → (A ∨ B) replace proposition variable P by B in 12
14 (B ∨ P) → (P ∨ B) replace proposition variable A by P in 13
15 (Q ∨ P) → (P ∨ Q) replace proposition variable B by Q in 14
16 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
17 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 16
18 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 17
19 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 18
20 (D → C) → (((Q ∨ ¬¬P) → D) → ((Q ∨ ¬¬P) → C)) replace proposition variable B by Q ∨ ¬¬P in 19
21 (D → (P ∨ Q)) → (((Q ∨ ¬¬P) → D) → ((Q ∨ ¬¬P) → (P ∨ Q))) replace proposition variable C by P ∨ Q in 20
22 ((Q ∨ P) → (P ∨ Q)) → (((Q ∨ ¬¬P) → (Q ∨ P)) → ((Q ∨ ¬¬P) → (P ∨ Q))) replace proposition variable D by Q ∨ P in 21
23 ((Q ∨ ¬¬P) → (Q ∨ P)) → ((Q ∨ ¬¬P) → (P ∨ Q)) modus ponens with 15, 22
24 (Q ∨ ¬¬P) → (P ∨ Q) modus ponens with 10, 23
25 (B ∨ Q) → (Q ∨ B) replace proposition variable A by Q in 13
26 (¬¬P ∨ Q) → (Q ∨ ¬¬P) replace proposition variable B by ¬¬P in 25
27 (D → C) → (((¬¬P ∨ Q) → D) → ((¬¬P ∨ Q) → C)) replace proposition variable B by ¬¬P ∨ Q in 19
28 (D → (P ∨ Q)) → (((¬¬P ∨ Q) → D) → ((¬¬P ∨ Q) → (P ∨ Q))) replace proposition variable C by P ∨ Q in 27
29 ((Q ∨ ¬¬P) → (P ∨ Q)) → (((¬¬P ∨ Q) → (Q ∨ ¬¬P)) → ((¬¬P ∨ Q) → (P ∨ Q))) replace proposition variable D by Q ∨ ¬¬P in 28
30 ((¬¬P ∨ Q) → (Q ∨ ¬¬P)) → ((¬¬P ∨ Q) → (P ∨ Q)) modus ponens with 24, 29
31 (¬¬P ∨ Q) → (P ∨ Q) modus ponens with 26, 30
32 (P → Q) → (¬Q → ¬P) add proposition hilb7
33 (P → A) → (¬A → ¬P) replace proposition variable Q by A in 32
34 (B → A) → (¬A → ¬B) replace proposition variable P by B in 33
35 (B → (P ∨ Q)) → (¬(P ∨ Q) → ¬B) replace proposition variable A by P ∨ Q in 34
36 ((¬¬P ∨ Q) → (P ∨ Q)) → (¬(P ∨ Q) → ¬(¬¬P ∨ Q)) replace proposition variable B by ¬¬P ∨ Q in 35
37 ¬(P ∨ Q) → ¬(¬¬P ∨ Q) modus ponens with 31, 36
38 (P → Q) → (¬P ∨ Q) add proposition defimpl1
39 (¬P ∨ Q) → (P → Q) add proposition defimpl2
40 (P → A) → (¬P ∨ A) replace proposition variable Q by A in 38
41 (B → A) → (¬B ∨ A) replace proposition variable P by B in 40
42 (¬P ∨ A) → (P → A) replace proposition variable Q by A in 39
43 (¬B ∨ A) → (B → A) replace proposition variable P by B in 42
44 (D → C) → ((¬¬P ∨ D) → (¬¬P ∨ C)) replace proposition variable B by ¬¬P in 6
45 (D → Q) → ((¬¬P ∨ D) → (¬¬P ∨ Q)) replace proposition variable C by Q in 44
46 (¬¬Q → Q) → ((¬¬P ∨ ¬¬Q) → (¬¬P ∨ Q)) replace proposition variable D by ¬¬Q in 45
47 (¬¬P ∨ ¬¬Q) → (¬¬P ∨ Q) modus ponens with 2, 46
48 (B → (¬¬P ∨ Q)) → (¬(¬¬P ∨ Q) → ¬B) replace proposition variable A by ¬¬P ∨ Q in 34
49 ((¬¬P ∨ ¬¬Q) → (¬¬P ∨ Q)) → (¬(¬¬P ∨ Q) → ¬(¬¬P ∨ ¬¬Q)) replace proposition variable B by ¬¬P ∨ ¬¬Q in 48
50 ¬(¬¬P ∨ Q) → ¬(¬¬P ∨ ¬¬Q) modus ponens with 47, 49
51 (D → C) → ((¬¬(P ∨ Q) ∨ D) → (¬¬(P ∨ Q) ∨ C)) replace proposition variable B by ¬¬(P ∨ Q) in 6
52 (D → ¬(¬¬P ∨ ¬¬Q)) → ((¬¬(P ∨ Q) ∨ D) → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q))) replace proposition variable C by ¬(¬¬P ∨ ¬¬Q) in 51
53 (¬(¬¬P ∨ Q) → ¬(¬¬P ∨ ¬¬Q)) → ((¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ Q)) → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q))) replace proposition variable D by ¬(¬¬P ∨ Q) in 52
54 (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ Q)) → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q)) modus ponens with 50, 53
55 (B → ¬(¬¬P ∨ Q)) → (¬B ∨ ¬(¬¬P ∨ Q)) replace proposition variable A by ¬(¬¬P ∨ Q) in 41
56 (¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ Q)) replace proposition variable B by ¬(P ∨ Q) in 55
57 (D → C) → (((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → D) → ((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → C)) replace proposition variable B by ¬(P ∨ Q) → ¬(¬¬P ∨ Q) in 19
58 (D → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q))) → (((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → D) → ((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q)))) replace proposition variable C by ¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q) in 57
59 ((¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ Q)) → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q))) → (((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ Q))) → ((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q)))) replace proposition variable D by ¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ Q) in 58
60 ((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ Q))) → ((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q))) modus ponens with 54, 59
61 (¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q)) modus ponens with 56, 60
62 (¬B ∨ ¬(¬¬P ∨ ¬¬Q)) → (B → ¬(¬¬P ∨ ¬¬Q)) replace proposition variable A by ¬(¬¬P ∨ ¬¬Q) in 43
63 (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q)) → (¬(P ∨ Q) → ¬(¬¬P ∨ ¬¬Q)) replace proposition variable B by ¬(P ∨ Q) in 62
64 (D → (¬(P ∨ Q) → ¬(¬¬P ∨ ¬¬Q))) → (((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → D) → ((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → (¬(P ∨ Q) → ¬(¬¬P ∨ ¬¬Q)))) replace proposition variable C by ¬(P ∨ Q) → ¬(¬¬P ∨ ¬¬Q) in 57
65 ((¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q)) → (¬(P ∨ Q) → ¬(¬¬P ∨ ¬¬Q))) → (((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q))) → ((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → (¬(P ∨ Q) → ¬(¬¬P ∨ ¬¬Q)))) replace proposition variable D by ¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q) in 64
66 ((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → (¬¬(P ∨ Q) ∨ ¬(¬¬P ∨ ¬¬Q))) → ((¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → (¬(P ∨ Q) → ¬(¬¬P ∨ ¬¬Q))) modus ponens with 63, 65
67 (¬(P ∨ Q) → ¬(¬¬P ∨ Q)) → (¬(P ∨ Q) → ¬(¬¬P ∨ ¬¬Q)) modus ponens with 61, 66
68 ¬(P ∨ Q) → ¬(¬¬P ∨ ¬¬Q) modus ponens with 37, 67
69 ¬(P ∨ Q) → (¬P ∧ ¬Q) reverse abbreviation and in 68 at occurence 1
qed

Reverse of a negation of a disjunction:

4. Proposition
      (¬P ∧ ¬Q) → ¬(P ∨ Q)     (hilb21)

Proof:
1 P → ¬¬P add proposition hilb5
2 Q → ¬¬Q replace proposition variable P by Q in 1
3 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
4 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 3
5 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 4
6 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 5
7 (D → C) → ((Q ∨ D) → (Q ∨ C)) replace proposition variable B by Q in 6
8 (D → ¬¬P) → ((Q ∨ D) → (Q ∨ ¬¬P)) replace proposition variable C by ¬¬P in 7
9 (P → ¬¬P) → ((Q ∨ P) → (Q ∨ ¬¬P)) replace proposition variable D by P in 8
10 (Q ∨ P) → (Q ∨ ¬¬P) modus ponens with 1, 9
11 (P ∨ Q) → (Q ∨ P) add axiom axiom3
12 (P ∨ A) → (A ∨ P) replace proposition variable Q by A in 11
13 (B ∨ A) → (A ∨ B) replace proposition variable P by B in 12
14 (B ∨ ¬¬P) → (¬¬P ∨ B) replace proposition variable A by ¬¬P in 13
15 (Q ∨ ¬¬P) → (¬¬P ∨ Q) replace proposition variable B by Q in 14
16 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
17 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 16
18 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 17
19 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 18
20 (D → C) → (((Q ∨ P) → D) → ((Q ∨ P) → C)) replace proposition variable B by Q ∨ P in 19
21 (D → (¬¬P ∨ Q)) → (((Q ∨ P) → D) → ((Q ∨ P) → (¬¬P ∨ Q))) replace proposition variable C by ¬¬P ∨ Q in 20
22 ((Q ∨ ¬¬P) → (¬¬P ∨ Q)) → (((Q ∨ P) → (Q ∨ ¬¬P)) → ((Q ∨ P) → (¬¬P ∨ Q))) replace proposition variable D by Q ∨ ¬¬P in 21
23 ((Q ∨ P) → (Q ∨ ¬¬P)) → ((Q ∨ P) → (¬¬P ∨ Q)) modus ponens with 15, 22
24 (Q ∨ P) → (¬¬P ∨ Q) modus ponens with 10, 23
25 (D → C) → (((P ∨ Q) → D) → ((P ∨ Q) → C)) replace proposition variable B by P ∨ Q in 19
26 (D → (¬¬P ∨ Q)) → (((P ∨ Q) → D) → ((P ∨ Q) → (¬¬P ∨ Q))) replace proposition variable C by ¬¬P ∨ Q in 25
27 ((Q ∨ P) → (¬¬P ∨ Q)) → (((P ∨ Q) → (Q ∨ P)) → ((P ∨ Q) → (¬¬P ∨ Q))) replace proposition variable D by Q ∨ P in 26
28 ((P ∨ Q) → (Q ∨ P)) → ((P ∨ Q) → (¬¬P ∨ Q)) modus ponens with 24, 27
29 (P ∨ Q) → (¬¬P ∨ Q) modus ponens with 11, 28
30 (P → Q) → (¬Q → ¬P) add proposition hilb7
31 (P → A) → (¬A → ¬P) replace proposition variable Q by A in 30
32 (B → A) → (¬A → ¬B) replace proposition variable P by B in 31
33 (B → (¬¬P ∨ Q)) → (¬(¬¬P ∨ Q) → ¬B) replace proposition variable A by ¬¬P ∨ Q in 32
34 ((P ∨ Q) → (¬¬P ∨ Q)) → (¬(¬¬P ∨ Q) → ¬(P ∨ Q)) replace proposition variable B by P ∨ Q in 33
35 ¬(¬¬P ∨ Q) → ¬(P ∨ Q) modus ponens with 29, 34
36 (P → Q) → (¬P ∨ Q) add proposition defimpl1
37 (¬P ∨ Q) → (P → Q) add proposition defimpl2
38 (B ∨ ¬(P ∨ Q)) → (¬(P ∨ Q) ∨ B) replace proposition variable A by ¬(P ∨ Q) in 13
39 (P → A) → (¬P ∨ A) replace proposition variable Q by A in 36
40 (B → A) → (¬B ∨ A) replace proposition variable P by B in 39
41 (B → ¬(P ∨ Q)) → (¬B ∨ ¬(P ∨ Q)) replace proposition variable A by ¬(P ∨ Q) in 40
42 (¬P ∨ A) → (P → A) replace proposition variable Q by A in 37
43 (¬B ∨ A) → (B → A) replace proposition variable P by B in 42
44 (¬B ∨ ¬(P ∨ Q)) → (B → ¬(P ∨ Q)) replace proposition variable A by ¬(P ∨ Q) in 43
45 (D → C) → ((¬¬P ∨ D) → (¬¬P ∨ C)) replace proposition variable B by ¬¬P in 6
46 (D → ¬¬Q) → ((¬¬P ∨ D) → (¬¬P ∨ ¬¬Q)) replace proposition variable C by ¬¬Q in 45
47 (Q → ¬¬Q) → ((¬¬P ∨ Q) → (¬¬P ∨ ¬¬Q)) replace proposition variable D by Q in 46
48 (¬¬P ∨ Q) → (¬¬P ∨ ¬¬Q) modus ponens with 2, 47
49 (B → (¬¬P ∨ ¬¬Q)) → (¬(¬¬P ∨ ¬¬Q) → ¬B) replace proposition variable A by ¬¬P ∨ ¬¬Q in 32
50 ((¬¬P ∨ Q) → (¬¬P ∨ ¬¬Q)) → (¬(¬¬P ∨ ¬¬Q) → ¬(¬¬P ∨ Q)) replace proposition variable B by ¬¬P ∨ Q in 49
51 ¬(¬¬P ∨ ¬¬Q) → ¬(¬¬P ∨ Q) modus ponens with 48, 50
52 (B → ¬(¬¬P ∨ Q)) → (¬¬(¬¬P ∨ Q) → ¬B) replace proposition variable A by ¬(¬¬P ∨ Q) in 32
53 (¬(¬¬P ∨ ¬¬Q) → ¬(¬¬P ∨ Q)) → (¬¬(¬¬P ∨ Q) → ¬¬(¬¬P ∨ ¬¬Q)) replace proposition variable B by ¬(¬¬P ∨ ¬¬Q) in 52
54 ¬¬(¬¬P ∨ Q) → ¬¬(¬¬P ∨ ¬¬Q) modus ponens with 51, 53
55 (D → C) → ((¬(P ∨ Q) ∨ D) → (¬(P ∨ Q) ∨ C)) replace proposition variable B by ¬(P ∨ Q) in 6
56 (D → ¬¬(¬¬P ∨ ¬¬Q)) → ((¬(P ∨ Q) ∨ D) → (¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ ¬¬Q))) replace proposition variable C by ¬¬(¬¬P ∨ ¬¬Q) in 55
57 (¬¬(¬¬P ∨ Q) → ¬¬(¬¬P ∨ ¬¬Q)) → ((¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q)) → (¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ ¬¬Q))) replace proposition variable D by ¬¬(¬¬P ∨ Q) in 56
58 (¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q)) → (¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ ¬¬Q)) modus ponens with 54, 57
59 (B ∨ ¬¬(¬¬P ∨ ¬¬Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ B) replace proposition variable A by ¬¬(¬¬P ∨ ¬¬Q) in 13
60 (¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ ¬¬Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q)) replace proposition variable B by ¬(P ∨ Q) in 59
61 (D → C) → (((¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q)) → D) → ((¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q)) → C)) replace proposition variable B by ¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q) in 19
62 (D → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q))) → (((¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q)) → D) → ((¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q)))) replace proposition variable C by ¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q) in 61
63 ((¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ ¬¬Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q))) → (((¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q)) → (¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ ¬¬Q))) → ((¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q)))) replace proposition variable D by ¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ ¬¬Q) in 62
64 ((¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q)) → (¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ ¬¬Q))) → ((¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q))) modus ponens with 60, 63
65 (¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q)) modus ponens with 58, 64
66 (¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q)) → (¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q)) replace proposition variable B by ¬¬(¬¬P ∨ Q) in 38
67 (D → C) → (((¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q)) → D) → ((¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q)) → C)) replace proposition variable B by ¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q) in 19
68 (D → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q))) → (((¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q)) → D) → ((¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q)))) replace proposition variable C by ¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q) in 67
69 ((¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q))) → (((¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q)) → (¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q))) → ((¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q)))) replace proposition variable D by ¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q) in 68
70 ((¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q)) → (¬(P ∨ Q) ∨ ¬¬(¬¬P ∨ Q))) → ((¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q))) modus ponens with 65, 69
71 (¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q)) modus ponens with 66, 70
72 (¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → (¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q)) replace proposition variable B by ¬(¬¬P ∨ Q) in 41
73 (D → C) → (((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → D) → ((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → C)) replace proposition variable B by ¬(¬¬P ∨ Q) → ¬(P ∨ Q) in 19
74 (D → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q))) → (((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → D) → ((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q)))) replace proposition variable C by ¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q) in 73
75 ((¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q))) → (((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → (¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q))) → ((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q)))) replace proposition variable D by ¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q) in 74
76 ((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → (¬¬(¬¬P ∨ Q) ∨ ¬(P ∨ Q))) → ((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q))) modus ponens with 71, 75
77 (¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q)) modus ponens with 72, 76
78 (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q)) → (¬(¬¬P ∨ ¬¬Q) → ¬(P ∨ Q)) replace proposition variable B by ¬(¬¬P ∨ ¬¬Q) in 44
79 (D → (¬(¬¬P ∨ ¬¬Q) → ¬(P ∨ Q))) → (((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → D) → ((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → (¬(¬¬P ∨ ¬¬Q) → ¬(P ∨ Q)))) replace proposition variable C by ¬(¬¬P ∨ ¬¬Q) → ¬(P ∨ Q) in 73
80 ((¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q)) → (¬(¬¬P ∨ ¬¬Q) → ¬(P ∨ Q))) → (((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q))) → ((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → (¬(¬¬P ∨ ¬¬Q) → ¬(P ∨ Q)))) replace proposition variable D by ¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q) in 79
81 ((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → (¬¬(¬¬P ∨ ¬¬Q) ∨ ¬(P ∨ Q))) → ((¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → (¬(¬¬P ∨ ¬¬Q) → ¬(P ∨ Q))) modus ponens with 78, 80
82 (¬(¬¬P ∨ Q) → ¬(P ∨ Q)) → (¬(¬¬P ∨ ¬¬Q) → ¬(P ∨ Q)) modus ponens with 77, 81
83 ¬(¬¬P ∨ ¬¬Q) → ¬(P ∨ Q) modus ponens with 35, 82
84 (¬P ∧ ¬Q) → ¬(P ∨ Q) reverse abbreviation and in 83 at occurence 1
qed

The Conjunction is commutative:

5. Proposition
      (P ∧ Q) → (Q ∧ P)     (hilb22)

Proof:
1 P → P add proposition hilb2
2 Q → Q replace proposition variable P by Q in 1
3 (P ∧ Q) → (P ∧ Q) replace proposition variable Q by P ∧ Q in 2
4 (P ∧ Q) → ¬(¬P ∨ ¬Q) use abbreviation and in 3 at occurence 2
5 (Q ∨ P) → (P ∨ Q) add proposition hilb10
6 (A ∨ P) → (P ∨ A) replace proposition variable Q by A in 5
7 (A ∨ B) → (B ∨ A) replace proposition variable P by B in 6
8 (¬Q ∨ B) → (B ∨ ¬Q) replace proposition variable A by ¬Q in 7
9 (¬Q ∨ ¬P) → (¬P ∨ ¬Q) replace proposition variable B by ¬P in 8
10 (P → Q) → (¬Q → ¬P) add proposition hilb7
11 (P → A) → (¬A → ¬P) replace proposition variable Q by A in 10
12 (B → A) → (¬A → ¬B) replace proposition variable P by B in 11
13 (B → (¬P ∨ ¬Q)) → (¬(¬P ∨ ¬Q) → ¬B) replace proposition variable A by ¬P ∨ ¬Q in 12
14 ((¬Q ∨ ¬P) → (¬P ∨ ¬Q)) → (¬(¬P ∨ ¬Q) → ¬(¬Q ∨ ¬P)) replace proposition variable B by ¬Q ∨ ¬P in 13
15 ¬(¬P ∨ ¬Q) → ¬(¬Q ∨ ¬P) modus ponens with 9, 14
16 (P → Q) → (¬P ∨ Q) add proposition defimpl1
17 (¬P ∨ Q) → (P → Q) add proposition defimpl2
18 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
19 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 18
20 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 19
21 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 20
22 (D → C) → ((¬(P ∧ Q) ∨ D) → (¬(P ∧ Q) ∨ C)) replace proposition variable B by ¬(P ∧ Q) in 21
23 (D → ¬(¬Q ∨ ¬P)) → ((¬(P ∧ Q) ∨ D) → (¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P))) replace proposition variable C by ¬(¬Q ∨ ¬P) in 22
24 (¬(¬P ∨ ¬Q) → ¬(¬Q ∨ ¬P)) → ((¬(P ∧ Q) ∨ ¬(¬P ∨ ¬Q)) → (¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P))) replace proposition variable D by ¬(¬P ∨ ¬Q) in 23
25 (¬(P ∧ Q) ∨ ¬(¬P ∨ ¬Q)) → (¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P)) modus ponens with 15, 24
26 (P → A) → (¬P ∨ A) replace proposition variable Q by A in 16
27 (B → A) → (¬B ∨ A) replace proposition variable P by B in 26
28 (B → ¬(¬P ∨ ¬Q)) → (¬B ∨ ¬(¬P ∨ ¬Q)) replace proposition variable A by ¬(¬P ∨ ¬Q) in 27
29 ((P ∧ Q) → ¬(¬P ∨ ¬Q)) → (¬(P ∧ Q) ∨ ¬(¬P ∨ ¬Q)) replace proposition variable B by P ∧ Q in 28
30 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
31 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 30
32 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 31
33 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 32
34 (D → C) → ((((P ∧ Q) → ¬(¬P ∨ ¬Q)) → D) → (((P ∧ Q) → ¬(¬P ∨ ¬Q)) → C)) replace proposition variable B by (P ∧ Q) → ¬(¬P ∨ ¬Q) in 33
35 (D → (¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P))) → ((((P ∧ Q) → ¬(¬P ∨ ¬Q)) → D) → (((P ∧ Q) → ¬(¬P ∨ ¬Q)) → (¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P)))) replace proposition variable C by ¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P) in 34
36 ((¬(P ∧ Q) ∨ ¬(¬P ∨ ¬Q)) → (¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P))) → ((((P ∧ Q) → ¬(¬P ∨ ¬Q)) → (¬(P ∧ Q) ∨ ¬(¬P ∨ ¬Q))) → (((P ∧ Q) → ¬(¬P ∨ ¬Q)) → (¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P)))) replace proposition variable D by ¬(P ∧ Q) ∨ ¬(¬P ∨ ¬Q) in 35
37 (((P ∧ Q) → ¬(¬P ∨ ¬Q)) → (¬(P ∧ Q) ∨ ¬(¬P ∨ ¬Q))) → (((P ∧ Q) → ¬(¬P ∨ ¬Q)) → (¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P))) modus ponens with 25, 36
38 ((P ∧ Q) → ¬(¬P ∨ ¬Q)) → (¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P)) modus ponens with 29, 37
39 (¬P ∨ A) → (P → A) replace proposition variable Q by A in 17
40 (¬B ∨ A) → (B → A) replace proposition variable P by B in 39
41 (¬B ∨ ¬(¬Q ∨ ¬P)) → (B → ¬(¬Q ∨ ¬P)) replace proposition variable A by ¬(¬Q ∨ ¬P) in 40
42 (¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P)) → ((P ∧ Q) → ¬(¬Q ∨ ¬P)) replace proposition variable B by P ∧ Q in 41
43 (D → ((P ∧ Q) → ¬(¬Q ∨ ¬P))) → ((((P ∧ Q) → ¬(¬P ∨ ¬Q)) → D) → (((P ∧ Q) → ¬(¬P ∨ ¬Q)) → ((P ∧ Q) → ¬(¬Q ∨ ¬P)))) replace proposition variable C by (P ∧ Q) → ¬(¬Q ∨ ¬P) in 34
44 ((¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P)) → ((P ∧ Q) → ¬(¬Q ∨ ¬P))) → ((((P ∧ Q) → ¬(¬P ∨ ¬Q)) → (¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P))) → (((P ∧ Q) → ¬(¬P ∨ ¬Q)) → ((P ∧ Q) → ¬(¬Q ∨ ¬P)))) replace proposition variable D by ¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P) in 43
45 (((P ∧ Q) → ¬(¬P ∨ ¬Q)) → (¬(P ∧ Q) ∨ ¬(¬Q ∨ ¬P))) → (((P ∧ Q) → ¬(¬P ∨ ¬Q)) → ((P ∧ Q) → ¬(¬Q ∨ ¬P))) modus ponens with 42, 44
46 ((P ∧ Q) → ¬(¬P ∨ ¬Q)) → ((P ∧ Q) → ¬(¬Q ∨ ¬P)) modus ponens with 38, 45
47 (P ∧ Q) → ¬(¬Q ∨ ¬P) modus ponens with 4, 46
48 (P ∧ Q) → (Q ∧ P) reverse abbreviation and in 47 at occurence 1
qed

A technical lemma that is simular to the previous one:

6. Proposition
      (Q ∧ P) → (P ∧ Q)     (hilb23)

Proof:
1 (P ∧ Q) → (Q ∧ P) add proposition hilb22
2 (P ∧ A) → (A ∧ P) replace proposition variable Q by A in 1
3 (B ∧ A) → (A ∧ B) replace proposition variable P by B in 2
4 (B ∧ P) → (P ∧ B) replace proposition variable A by P in 3
5 (Q ∧ P) → (P ∧ Q) replace proposition variable B by Q in 4
qed

Reduction of a conjunction:

7. Proposition
      (P ∧ Q) → P     (hilb24)

Proof:
1 P → (P ∨ Q) add axiom axiom2
2 P → (P ∨ A) replace proposition variable Q by A in 1
3 B → (B ∨ A) replace proposition variable P by B in 2
4 B → (B ∨ ¬Q) replace proposition variable A by ¬Q in 3
5 ¬P → (¬P ∨ ¬Q) replace proposition variable B by ¬P in 4
6 (P → Q) → (¬Q → ¬P) add proposition hilb7
7 (P → A) → (¬A → ¬P) replace proposition variable Q by A in 6
8 (B → A) → (¬A → ¬B) replace proposition variable P by B in 7
9 (B → (¬P ∨ ¬Q)) → (¬(¬P ∨ ¬Q) → ¬B) replace proposition variable A by ¬P ∨ ¬Q in 8
10 (¬P → (¬P ∨ ¬Q)) → (¬(¬P ∨ ¬Q) → ¬¬P) replace proposition variable B by ¬P in 9
11 ¬(¬P ∨ ¬Q) → ¬¬P modus ponens with 5, 10
12 (P ∧ Q) → ¬¬P reverse abbreviation and in 11 at occurence 1
13 ¬¬P → P add proposition hilb6
14 (P → Q) → (¬P ∨ Q) add proposition defimpl1
15 (¬P ∨ Q) → (P → Q) add proposition defimpl2
16 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
17 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 16
18 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 17
19 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 18
20 (D → C) → ((¬(P ∧ Q) ∨ D) → (¬(P ∧ Q) ∨ C)) replace proposition variable B by ¬(P ∧ Q) in 19
21 (D → P) → ((¬(P ∧ Q) ∨ D) → (¬(P ∧ Q) ∨ P)) replace proposition variable C by P in 20
22 (¬¬P → P) → ((¬(P ∧ Q) ∨ ¬¬P) → (¬(P ∧ Q) ∨ P)) replace proposition variable D by ¬¬P in 21
23 (¬(P ∧ Q) ∨ ¬¬P) → (¬(P ∧ Q) ∨ P) modus ponens with 13, 22
24 (P → A) → (¬P ∨ A) replace proposition variable Q by A in 14
25 (B → A) → (¬B ∨ A) replace proposition variable P by B in 24
26 (B → ¬¬P) → (¬B ∨ ¬¬P) replace proposition variable A by ¬¬P in 25
27 ((P ∧ Q) → ¬¬P) → (¬(P ∧ Q) ∨ ¬¬P) replace proposition variable B by P ∧ Q in 26
28 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
29 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 28
30 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 29
31 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 30
32 (D → C) → ((((P ∧ Q) → ¬¬P) → D) → (((P ∧ Q) → ¬¬P) → C)) replace proposition variable B by (P ∧ Q) → ¬¬P in 31
33 (D → (¬(P ∧ Q) ∨ P)) → ((((P ∧ Q) → ¬¬P) → D) → (((P ∧ Q) → ¬¬P) → (¬(P ∧ Q) ∨ P))) replace proposition variable C by ¬(P ∧ Q) ∨ P in 32
34 ((¬(P ∧ Q) ∨ ¬¬P) → (¬(P ∧ Q) ∨ P)) → ((((P ∧ Q) → ¬¬P) → (¬(P ∧ Q) ∨ ¬¬P)) → (((P ∧ Q) → ¬¬P) → (¬(P ∧ Q) ∨ P))) replace proposition variable D by ¬(P ∧ Q) ∨ ¬¬P in 33
35 (((P ∧ Q) → ¬¬P) → (¬(P ∧ Q) ∨ ¬¬P)) → (((P ∧ Q) → ¬¬P) → (¬(P ∧ Q) ∨ P)) modus ponens with 23, 34
36 ((P ∧ Q) → ¬¬P) → (¬(P ∧ Q) ∨ P) modus ponens with 27, 35
37 (¬P ∨ A) → (P → A) replace proposition variable Q by A in 15
38 (¬B ∨ A) → (B → A) replace proposition variable P by B in 37
39 (¬B ∨ P) → (B → P) replace proposition variable A by P in 38
40 (¬(P ∧ Q) ∨ P) → ((P ∧ Q) → P) replace proposition variable B by P ∧ Q in 39
41 (D → ((P ∧ Q) → P)) → ((((P ∧ Q) → ¬¬P) → D) → (((P ∧ Q) → ¬¬P) → ((P ∧ Q) → P))) replace proposition variable C by (P ∧ Q) → P in 32
42 ((¬(P ∧ Q) ∨ P) → ((P ∧ Q) → P)) → ((((P ∧ Q) → ¬¬P) → (¬(P ∧ Q) ∨ P)) → (((P ∧ Q) → ¬¬P) → ((P ∧ Q) → P))) replace proposition variable D by ¬(P ∧ Q) ∨ P in 41
43 (((P ∧ Q) → ¬¬P) → (¬(P ∧ Q) ∨ P)) → (((P ∧ Q) → ¬¬P) → ((P ∧ Q) → P)) modus ponens with 40, 42
44 ((P ∧ Q) → ¬¬P) → ((P ∧ Q) → P) modus ponens with 36, 43
45 (P ∧ Q) → P modus ponens with 12, 44
qed

Another form of a reduction of a conjunction:

8. Proposition
      (P ∧ Q) → Q     (hilb25)

Proof:
1 (P ∧ Q) → P add proposition hilb24
2 (P ∧ A) → P replace proposition variable Q by A in 1
3 (B ∧ A) → B replace proposition variable P by B in 2
4 (B ∧ P) → B replace proposition variable A by P in 3
5 (Q ∧ P) → Q replace proposition variable B by Q in 4
6 (Q ∧ P) → (P ∧ Q) add proposition hilb23
7 (A ∧ P) → (P ∧ A) replace proposition variable Q by A in 6
8 (A ∧ B) → (B ∧ A) replace proposition variable P by B in 7
9 (P ∧ B) → (B ∧ P) replace proposition variable A by P in 8
10 (P ∧ Q) → (Q ∧ P) replace proposition variable B by Q in 9
11 (P → Q) → (¬P ∨ Q) add proposition defimpl1
12 (¬P ∨ Q) → (P → Q) add proposition defimpl2
13 (P → Q) → (¬Q → ¬P) add proposition hilb7
14 (P → A) → (¬A → ¬P) replace proposition variable Q by A in 13
15 (B → A) → (¬A → ¬B) replace proposition variable P by B in 14
16 (B → (Q ∧ P)) → (¬(Q ∧ P) → ¬B) replace proposition variable A by Q ∧ P in 15
17 ((P ∧ Q) → (Q ∧ P)) → (¬(Q ∧ P) → ¬(P ∧ Q)) replace proposition variable B by P ∧ Q in 16
18 ¬(Q ∧ P) → ¬(P ∧ Q) modus ponens with 10, 17
19 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
20 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 19
21 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 20
22 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 21
23 (D → C) → ((Q ∨ D) → (Q ∨ C)) replace proposition variable B by Q in 22
24 (D → ¬(P ∧ Q)) → ((Q ∨ D) → (Q ∨ ¬(P ∧ Q))) replace proposition variable C by ¬(P ∧ Q) in 23
25 (¬(Q ∧ P) → ¬(P ∧ Q)) → ((Q ∨ ¬(Q ∧ P)) → (Q ∨ ¬(P ∧ Q))) replace proposition variable D by ¬(Q ∧ P) in 24
26 (Q ∨ ¬(Q ∧ P)) → (Q ∨ ¬(P ∧ Q)) modus ponens with 18, 25
27 (P ∨ Q) → (Q ∨ P) add axiom axiom3
28 (P ∨ A) → (A ∨ P) replace proposition variable Q by A in 27
29 (B ∨ A) → (A ∨ B) replace proposition variable P by B in 28
30 (B ∨ ¬(P ∧ Q)) → (¬(P ∧ Q) ∨ B) replace proposition variable A by ¬(P ∧ Q) in 29
31 (Q ∨ ¬(P ∧ Q)) → (¬(P ∧ Q) ∨ Q) replace proposition variable B by Q in 30
32 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
33 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 32
34 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 33
35 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 34
36 (D → C) → (((Q ∨ ¬(Q ∧ P)) → D) → ((Q ∨ ¬(Q ∧ P)) → C)) replace proposition variable B by Q ∨ ¬(Q ∧ P) in 35
37 (D → (¬(P ∧ Q) ∨ Q)) → (((Q ∨ ¬(Q ∧ P)) → D) → ((Q ∨ ¬(Q ∧ P)) → (¬(P ∧ Q) ∨ Q))) replace proposition variable C by ¬(P ∧ Q) ∨ Q in 36
38 ((Q ∨ ¬(P ∧ Q)) → (¬(P ∧ Q) ∨ Q)) → (((Q ∨ ¬(Q ∧ P)) → (Q ∨ ¬(P ∧ Q))) → ((Q ∨ ¬(Q ∧ P)) → (¬(P ∧ Q) ∨ Q))) replace proposition variable D by Q ∨ ¬(P ∧ Q) in 37
39 ((Q ∨ ¬(Q ∧ P)) → (Q ∨ ¬(P ∧ Q))) → ((Q ∨ ¬(Q ∧ P)) → (¬(P ∧ Q) ∨ Q)) modus ponens with 31, 38
40 (Q ∨ ¬(Q ∧ P)) → (¬(P ∧ Q) ∨ Q) modus ponens with 26, 39
41 (B ∨ Q) → (Q ∨ B) replace proposition variable A by Q in 29
42 (¬(Q ∧ P) ∨ Q) → (Q ∨ ¬(Q ∧ P)) replace proposition variable B by ¬(Q ∧ P) in 41
43 (D → C) → (((¬(Q ∧ P) ∨ Q) → D) → ((¬(Q ∧ P) ∨ Q) → C)) replace proposition variable B by ¬(Q ∧ P) ∨ Q in 35
44 (D → (¬(P ∧ Q) ∨ Q)) → (((¬(Q ∧ P) ∨ Q) → D) → ((¬(Q ∧ P) ∨ Q) → (¬(P ∧ Q) ∨ Q))) replace proposition variable C by ¬(P ∧ Q) ∨ Q in 43
45 ((Q ∨ ¬(Q ∧ P)) → (¬(P ∧ Q) ∨ Q)) → (((¬(Q ∧ P) ∨ Q) → (Q ∨ ¬(Q ∧ P))) → ((¬(Q ∧ P) ∨ Q) → (¬(P ∧ Q) ∨ Q))) replace proposition variable D by Q ∨ ¬(Q ∧ P) in 44
46 ((¬(Q ∧ P) ∨ Q) → (Q ∨ ¬(Q ∧ P))) → ((¬(Q ∧ P) ∨ Q) → (¬(P ∧ Q) ∨ Q)) modus ponens with 40, 45
47 (¬(Q ∧ P) ∨ Q) → (¬(P ∧ Q) ∨ Q) modus ponens with 42, 46
48 (P → A) → (¬P ∨ A) replace proposition variable Q by A in 11
49 (B → A) → (¬B ∨ A) replace proposition variable P by B in 48
50 (B → Q) → (¬B ∨ Q) replace proposition variable A by Q in 49
51 ((Q ∧ P) → Q) → (¬(Q ∧ P) ∨ Q) replace proposition variable B by Q ∧ P in 50
52 (D → C) → ((((Q ∧ P) → Q) → D) → (((Q ∧ P) → Q) → C)) replace proposition variable B by (Q ∧ P) → Q in 35
53 (D → (¬(P ∧ Q) ∨ Q)) → ((((Q ∧ P) → Q) → D) → (((Q ∧ P) → Q) → (¬(P ∧ Q) ∨ Q))) replace proposition variable C by ¬(P ∧ Q) ∨ Q in 52
54 ((¬(Q ∧ P) ∨ Q) → (¬(P ∧ Q) ∨ Q)) → ((((Q ∧ P) → Q) → (¬(Q ∧ P) ∨ Q)) → (((Q ∧ P) → Q) → (¬(P ∧ Q) ∨ Q))) replace proposition variable D by ¬(Q ∧ P) ∨ Q in 53
55 (((Q ∧ P) → Q) → (¬(Q ∧ P) ∨ Q)) → (((Q ∧ P) → Q) → (¬(P ∧ Q) ∨ Q)) modus ponens with 47, 54
56 ((Q ∧ P) → Q) → (¬(P ∧ Q) ∨ Q) modus ponens with 51, 55
57 (¬P ∨ A) → (P → A) replace proposition variable Q by A in 12
58 (¬B ∨ A) → (B → A) replace proposition variable P by B in 57
59 (¬B ∨ Q) → (B → Q) replace proposition variable A by Q in 58
60 (¬(P ∧ Q) ∨ Q) → ((P ∧ Q) → Q) replace proposition variable B by P ∧ Q in 59
61 (D → ((P ∧ Q) → Q)) → ((((Q ∧ P) → Q) → D) → (((Q ∧ P) → Q) → ((P ∧ Q) → Q))) replace proposition variable C by (P ∧ Q) → Q in 52
62 ((¬(P ∧ Q) ∨ Q) → ((P ∧ Q) → Q)) → ((((Q ∧ P) → Q) → (¬(P ∧ Q) ∨ Q)) → (((Q ∧ P) → Q) → ((P ∧ Q) → Q))) replace proposition variable D by ¬(P ∧ Q) ∨ Q in 61
63 (((Q ∧ P) → Q) → (¬(P ∧ Q) ∨ Q)) → (((Q ∧ P) → Q) → ((P ∧ Q) → Q)) modus ponens with 60, 62
64 ((Q ∧ P) → Q) → ((P ∧ Q) → Q) modus ponens with 56, 63
65 (P ∧ Q) → Q modus ponens with 5, 64
qed

The conjunction is associative too (first implication):

9. Proposition
      (P ∧ (Q ∧ A)) → ((P ∧ Q) ∧ A)     (hilb26)

Proof:
1 ((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)) add proposition hilb15
2 (P → Q) → (¬Q → ¬P) add proposition hilb7
3 (P → A) → (¬A → ¬P) replace proposition variable Q by A in 2
4 (B → A) → (¬A → ¬B) replace proposition variable P by B in 3
5 (B → (P ∨ (Q ∨ A))) → (¬(P ∨ (Q ∨ A)) → ¬B) replace proposition variable A by P ∨ (Q ∨ A) in 4
6 (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A))) → (¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) replace proposition variable B by (P ∨ Q) ∨ A in 5
7 ¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A) modus ponens with 1, 6
8 P → ¬¬P add proposition hilb5
9 B → ¬¬B replace proposition variable P by B in 8
10 (Q ∨ A) → ¬¬(Q ∨ A) replace proposition variable B by Q ∨ A in 9
11 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
12 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 11
13 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 12
14 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 13
15 (D → C) → ((P ∨ D) → (P ∨ C)) replace proposition variable B by P in 14
16 (D → ¬¬(Q ∨ A)) → ((P ∨ D) → (P ∨ ¬¬(Q ∨ A))) replace proposition variable C by ¬¬(Q ∨ A) in 15
17 ((Q ∨ A) → ¬¬(Q ∨ A)) → ((P ∨ (Q ∨ A)) → (P ∨ ¬¬(Q ∨ A))) replace proposition variable D by Q ∨ A in 16
18 (P ∨ (Q ∨ A)) → (P ∨ ¬¬(Q ∨ A)) modus ponens with 10, 17
19 (P → B) → (¬B → ¬P) replace proposition variable Q by B in 2
20 (C → B) → (¬B → ¬C) replace proposition variable P by C in 19
21 (C → (P ∨ ¬¬(Q ∨ A))) → (¬(P ∨ ¬¬(Q ∨ A)) → ¬C) replace proposition variable B by P ∨ ¬¬(Q ∨ A) in 20
22 ((P ∨ (Q ∨ A)) → (P ∨ ¬¬(Q ∨ A))) → (¬(P ∨ ¬¬(Q ∨ A)) → ¬(P ∨ (Q ∨ A))) replace proposition variable C by P ∨ (Q ∨ A) in 21
23 ¬(P ∨ ¬¬(Q ∨ A)) → ¬(P ∨ (Q ∨ A)) modus ponens with 18, 22
24 (P → Q) → (¬P ∨ Q) add proposition defimpl1
25 (¬P ∨ Q) → (P → Q) add proposition defimpl2
26 (C → ¬(P ∨ (Q ∨ A))) → (¬¬(P ∨ (Q ∨ A)) → ¬C) replace proposition variable B by ¬(P ∨ (Q ∨ A)) in 20
27 (¬(P ∨ ¬¬(Q ∨ A)) → ¬(P ∨ (Q ∨ A))) → (¬¬(P ∨ (Q ∨ A)) → ¬¬(P ∨ ¬¬(Q ∨ A))) replace proposition variable C by ¬(P ∨ ¬¬(Q ∨ A)) in 26
28 ¬¬(P ∨ (Q ∨ A)) → ¬¬(P ∨ ¬¬(Q ∨ A)) modus ponens with 23, 27
29 (D → C) → ((¬((P ∨ Q) ∨ A) ∨ D) → (¬((P ∨ Q) ∨ A) ∨ C)) replace proposition variable B by ¬((P ∨ Q) ∨ A) in 14
30 (D → ¬¬(P ∨ ¬¬(Q ∨ A))) → ((¬((P ∨ Q) ∨ A) ∨ D) → (¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ ¬¬(Q ∨ A)))) replace proposition variable C by ¬¬(P ∨ ¬¬(Q ∨ A)) in 29
31 (¬¬(P ∨ (Q ∨ A)) → ¬¬(P ∨ ¬¬(Q ∨ A))) → ((¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A))) → (¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ ¬¬(Q ∨ A)))) replace proposition variable D by ¬¬(P ∨ (Q ∨ A)) in 30
32 (¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A))) → (¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ ¬¬(Q ∨ A))) modus ponens with 28, 31
33 (P ∨ Q) → (Q ∨ P) add axiom axiom3
34 (P ∨ B) → (B ∨ P) replace proposition variable Q by B in 33
35 (C ∨ B) → (B ∨ C) replace proposition variable P by C in 34
36 (C ∨ ¬¬(P ∨ ¬¬(Q ∨ A))) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ C) replace proposition variable B by ¬¬(P ∨ ¬¬(Q ∨ A)) in 35
37 (¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ ¬¬(Q ∨ A))) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) replace proposition variable C by ¬((P ∨ Q) ∨ A) in 36
38 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
39 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 38
40 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 39
41 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 40
42 (D → C) → (((¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A))) → D) → ((¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A))) → C)) replace proposition variable B by ¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A)) in 41
43 (D → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A))) → (((¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A))) → D) → ((¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A))) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)))) replace proposition variable C by ¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A) in 42
44 ((¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ ¬¬(Q ∨ A))) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A))) → (((¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A))) → (¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ ¬¬(Q ∨ A)))) → ((¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A))) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)))) replace proposition variable D by ¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ ¬¬(Q ∨ A)) in 43
45 ((¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A))) → (¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ ¬¬(Q ∨ A)))) → ((¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A))) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A))) modus ponens with 37, 44
46 (¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A))) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) modus ponens with 32, 45
47 (C ∨ ¬((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ C) replace proposition variable B by ¬((P ∨ Q) ∨ A) in 35
48 (¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A))) replace proposition variable C by ¬¬(P ∨ (Q ∨ A)) in 47
49 (D → C) → (((¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → D) → ((¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → C)) replace proposition variable B by ¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A) in 41
50 (D → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A))) → (((¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → D) → ((¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)))) replace proposition variable C by ¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A) in 49
51 ((¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A))) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A))) → (((¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A)))) → ((¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)))) replace proposition variable D by ¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A)) in 50
52 ((¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ¬¬(P ∨ (Q ∨ A)))) → ((¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A))) modus ponens with 46, 51
53 (¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) modus ponens with 48, 52
54 (P → B) → (¬P ∨ B) replace proposition variable Q by B in 24
55 (C → B) → (¬C ∨ B) replace proposition variable P by C in 54
56 (C → ¬((P ∨ Q) ∨ A)) → (¬C ∨ ¬((P ∨ Q) ∨ A)) replace proposition variable B by ¬((P ∨ Q) ∨ A) in 55
57 (¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) replace proposition variable C by ¬(P ∨ (Q ∨ A)) in 56
58 (D → C) → (((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → D) → ((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → C)) replace proposition variable B by ¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A) in 41
59 (D → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A))) → (((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → D) → ((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)))) replace proposition variable C by ¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A) in 58
60 ((¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A))) → (((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A))) → ((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)))) replace proposition variable D by ¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A) in 59
61 ((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ (Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A))) → ((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A))) modus ponens with 53, 60
62 (¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) modus ponens with 57, 61
63 (¬P ∨ B) → (P → B) replace proposition variable Q by B in 25
64 (¬C ∨ B) → (C → B) replace proposition variable P by C in 63
65 (¬C ∨ ¬((P ∨ Q) ∨ A)) → (C → ¬((P ∨ Q) ∨ A)) replace proposition variable B by ¬((P ∨ Q) ∨ A) in 64
66 (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → (¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A)) replace proposition variable C by ¬(P ∨ ¬¬(Q ∨ A)) in 65
67 (D → (¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A))) → (((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → D) → ((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A)))) replace proposition variable C by ¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A) in 58
68 ((¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → (¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A))) → (((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A))) → ((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A)))) replace proposition variable D by ¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A) in 67
69 ((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A))) → ((¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A))) modus ponens with 66, 68
70 (¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A)) modus ponens with 62, 69
71 ¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A) modus ponens with 7, 70
72 ¬¬P → P add proposition hilb6
73 ¬¬A → A replace proposition variable P by A in 72
74 ¬¬(P ∨ Q) → (P ∨ Q) replace proposition variable A by P ∨ Q in 73
75 (D → C) → ((A ∨ D) → (A ∨ C)) replace proposition variable B by A in 14
76 (D → (P ∨ Q)) → ((A ∨ D) → (A ∨ (P ∨ Q))) replace proposition variable C by P ∨ Q in 75
77 (¬¬(P ∨ Q) → (P ∨ Q)) → ((A ∨ ¬¬(P ∨ Q)) → (A ∨ (P ∨ Q))) replace proposition variable D by ¬¬(P ∨ Q) in 76
78 (A ∨ ¬¬(P ∨ Q)) → (A ∨ (P ∨ Q)) modus ponens with 74, 77
79 (C ∨ (P ∨ Q)) → ((P ∨ Q) ∨ C) replace proposition variable B by P ∨ Q in 35
80 (A ∨ (P ∨ Q)) → ((P ∨ Q) ∨ A) replace proposition variable C by A in 79
81 (D → C) → (((A ∨ ¬¬(P ∨ Q)) → D) → ((A ∨ ¬¬(P ∨ Q)) → C)) replace proposition variable B by A ∨ ¬¬(P ∨ Q) in 41
82 (D → ((P ∨ Q) ∨ A)) → (((A ∨ ¬¬(P ∨ Q)) → D) → ((A ∨ ¬¬(P ∨ Q)) → ((P ∨ Q) ∨ A))) replace proposition variable C by (P ∨ Q) ∨ A in 81
83 ((A ∨ (P ∨ Q)) → ((P ∨ Q) ∨ A)) → (((A ∨ ¬¬(P ∨ Q)) → (A ∨ (P ∨ Q))) → ((A ∨ ¬¬(P ∨ Q)) → ((P ∨ Q) ∨ A))) replace proposition variable D by A ∨ (P ∨ Q) in 82
84 ((A ∨ ¬¬(P ∨ Q)) → (A ∨ (P ∨ Q))) → ((A ∨ ¬¬(P ∨ Q)) → ((P ∨ Q) ∨ A)) modus ponens with 80, 83
85 (A ∨ ¬¬(P ∨ Q)) → ((P ∨ Q) ∨ A) modus ponens with 78, 84
86 (C ∨ A) → (A ∨ C) replace proposition variable B by A in 35
87 (¬¬(P ∨ Q) ∨ A) → (A ∨ ¬¬(P ∨ Q)) replace proposition variable C by ¬¬(P ∨ Q) in 86
88 (D → C) → (((¬¬(P ∨ Q) ∨ A) → D) → ((¬¬(P ∨ Q) ∨ A) → C)) replace proposition variable B by ¬¬(P ∨ Q) ∨ A in 41
89 (D → ((P ∨ Q) ∨ A)) → (((¬¬(P ∨ Q) ∨ A) → D) → ((¬¬(P ∨ Q) ∨ A) → ((P ∨ Q) ∨ A))) replace proposition variable C by (P ∨ Q) ∨ A in 88
90 ((A ∨ ¬¬(P ∨ Q)) → ((P ∨ Q) ∨ A)) → (((¬¬(P ∨ Q) ∨ A) → (A ∨ ¬¬(P ∨ Q))) → ((¬¬(P ∨ Q) ∨ A) → ((P ∨ Q) ∨ A))) replace proposition variable D by A ∨ ¬¬(P ∨ Q) in 89
91 ((¬¬(P ∨ Q) ∨ A) → (A ∨ ¬¬(P ∨ Q))) → ((¬¬(P ∨ Q) ∨ A) → ((P ∨ Q) ∨ A)) modus ponens with 85, 90
92 (¬¬(P ∨ Q) ∨ A) → ((P ∨ Q) ∨ A) modus ponens with 87, 91
93 (C → ((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) → ¬C) replace proposition variable B by (P ∨ Q) ∨ A in 20
94 ((¬¬(P ∨ Q) ∨ A) → ((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) → ¬(¬¬(P ∨ Q) ∨ A)) replace proposition variable C by ¬¬(P ∨ Q) ∨ A in 93
95 ¬((P ∨ Q) ∨ A) → ¬(¬¬(P ∨ Q) ∨ A) modus ponens with 92, 94
96 (D → C) → ((¬¬(P ∨ ¬¬(Q ∨ A)) ∨ D) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ C)) replace proposition variable B by ¬¬(P ∨ ¬¬(Q ∨ A)) in 14
97 (D → ¬(¬¬(P ∨ Q) ∨ A)) → ((¬¬(P ∨ ¬¬(Q ∨ A)) ∨ D) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬(¬¬(P ∨ Q) ∨ A))) replace proposition variable C by ¬(¬¬(P ∨ Q) ∨ A) in 96
98 (¬((P ∨ Q) ∨ A) → ¬(¬¬(P ∨ Q) ∨ A)) → ((¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬(¬¬(P ∨ Q) ∨ A))) replace proposition variable D by ¬((P ∨ Q) ∨ A) in 97
99 (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬(¬¬(P ∨ Q) ∨ A)) modus ponens with 95, 98
100 (¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬((P ∨ Q) ∨ A)) replace proposition variable C by ¬(P ∨ ¬¬(Q ∨ A)) in 56
101 (D → C) → (((¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → D) → ((¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → C)) replace proposition variable B by ¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A) in 41
102