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 (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 101
103 ((¬¬(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 102
104 ((¬(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 99, 103
105 (¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬(¬¬(P ∨ Q) ∨ A)) modus ponens with 100, 104
106 (¬C ∨ ¬(¬¬(P ∨ Q) ∨ A)) → (C → ¬(¬¬(P ∨ Q) ∨ A)) replace proposition variable B by ¬(¬¬(P ∨ Q) ∨ A) in 64
107 (¬¬(P ∨ ¬¬(Q ∨ A)) ∨ ¬(¬¬(P ∨ Q) ∨ A)) → (¬(P ∨ ¬¬(Q ∨ A)) → ¬(¬¬(P ∨ Q) ∨ A)) replace proposition variable C by ¬(P ∨ ¬¬(Q ∨ A)) in 106
108 (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 101
109 ((¬¬(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 108
110 ((¬(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 107, 109
111 (¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A)) → (¬(P ∨ ¬¬(Q ∨ A)) → ¬(¬¬(P ∨ Q) ∨ A)) modus ponens with 105, 110
112 ¬(P ∨ ¬¬(Q ∨ A)) → ¬(¬¬(P ∨ Q) ∨ A) modus ponens with 71, 111
113 ¬(P ∨ ¬¬(Q ∨ B)) → ¬(¬¬(P ∨ Q) ∨ B) replace proposition variable A by B in 112
114 ¬(P ∨ ¬¬(C ∨ B)) → ¬(¬¬(P ∨ C) ∨ B) replace proposition variable Q by C in 113
115 ¬(D ∨ ¬¬(C ∨ B)) → ¬(¬¬(D ∨ C) ∨ B) replace proposition variable P by D in 114
116 ¬(D ∨ ¬¬(C ∨ ¬A)) → ¬(¬¬(D ∨ C) ∨ ¬A) replace proposition variable B by ¬A in 115
117 ¬(D ∨ ¬¬(¬Q ∨ ¬A)) → ¬(¬¬(D ∨ ¬Q) ∨ ¬A) replace proposition variable C by ¬Q in 116
118 ¬(¬P ∨ ¬¬(¬Q ∨ ¬A)) → ¬(¬¬(¬P ∨ ¬Q) ∨ ¬A) replace proposition variable D by ¬P in 117
119 (P ∧ ¬(¬Q ∨ ¬A)) → ¬(¬¬(¬P ∨ ¬Q) ∨ ¬A) reverse abbreviation and in 118 at occurence 1
120 (P ∧ (Q ∧ A)) → ¬(¬¬(¬P ∨ ¬Q) ∨ ¬A) reverse abbreviation and in 119 at occurence 1
121 (P ∧ (Q ∧ A)) → (¬(¬P ∨ ¬Q) ∧ A) reverse abbreviation and in 120 at occurence 1
122 (P ∧ (Q ∧ A)) → ((P ∧ Q) ∧ A) reverse abbreviation and in 121 at occurence 1
qed

The conjunction is associative (second implication):

10. Proposition
      ((P ∧ Q) ∧ A) → (P ∧ (Q ∧ A))     (hilb27)

Proof:
1 (P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A) add proposition hilb14
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 A → ¬¬A replace proposition variable P by A in 8
10 (P ∨ Q) → ¬¬(P ∨ Q) replace proposition variable A by P ∨ Q 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) → ((A ∨ D) → (A ∨ C)) replace proposition variable B by A in 14
16 (D → ¬¬(P ∨ Q)) → ((A ∨ D) → (A ∨ ¬¬(P ∨ Q))) replace proposition variable C by ¬¬(P ∨ Q) in 15
17 ((P ∨ Q) → ¬¬(P ∨ Q)) → ((A ∨ (P ∨ Q)) → (A ∨ ¬¬(P ∨ Q))) replace proposition variable D by P ∨ Q in 16
18 (A ∨ (P ∨ Q)) → (A ∨ ¬¬(P ∨ Q)) modus ponens with 10, 17
19 (P ∨ Q) → (Q ∨ P) add axiom axiom3
20 (P ∨ B) → (B ∨ P) replace proposition variable Q by B in 19
21 (C ∨ B) → (B ∨ C) replace proposition variable P by C in 20
22 (C ∨ ¬¬(P ∨ Q)) → (¬¬(P ∨ Q) ∨ C) replace proposition variable B by ¬¬(P ∨ Q) in 21
23 (A ∨ ¬¬(P ∨ Q)) → (¬¬(P ∨ Q) ∨ A) replace proposition variable C by A in 22
24 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
25 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 24
26 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 25
27 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 26
28 (D → C) → (((A ∨ (P ∨ Q)) → D) → ((A ∨ (P ∨ Q)) → C)) replace proposition variable B by A ∨ (P ∨ Q) in 27
29 (D → (¬¬(P ∨ Q) ∨ A)) → (((A ∨ (P ∨ Q)) → D) → ((A ∨ (P ∨ Q)) → (¬¬(P ∨ Q) ∨ A))) replace proposition variable C by ¬¬(P ∨ Q) ∨ A in 28
30 ((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 29
31 ((A ∨ (P ∨ Q)) → (A ∨ ¬¬(P ∨ Q))) → ((A ∨ (P ∨ Q)) → (¬¬(P ∨ Q) ∨ A)) modus ponens with 23, 30
32 (A ∨ (P ∨ Q)) → (¬¬(P ∨ Q) ∨ A) modus ponens with 18, 31
33 (C ∨ A) → (A ∨ C) replace proposition variable B by A in 21
34 ((P ∨ Q) ∨ A) → (A ∨ (P ∨ Q)) replace proposition variable C by P ∨ Q in 33
35 (D → C) → ((((P ∨ Q) ∨ A) → D) → (((P ∨ Q) ∨ A) → C)) replace proposition variable B by (P ∨ Q) ∨ A in 27
36 (D → (¬¬(P ∨ Q) ∨ A)) → ((((P ∨ Q) ∨ A) → D) → (((P ∨ Q) ∨ A) → (¬¬(P ∨ Q) ∨ A))) replace proposition variable C by ¬¬(P ∨ Q) ∨ A in 35
37 ((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 36
38 (((P ∨ Q) ∨ A) → (A ∨ (P ∨ Q))) → (((P ∨ Q) ∨ A) → (¬¬(P ∨ Q) ∨ A)) modus ponens with 32, 37
39 ((P ∨ Q) ∨ A) → (¬¬(P ∨ Q) ∨ A) modus ponens with 34, 38
40 (P → B) → (¬B → ¬P) replace proposition variable Q by B in 2
41 (C → B) → (¬B → ¬C) replace proposition variable P by C in 40
42 (C → (¬¬(P ∨ Q) ∨ A)) → (¬(¬¬(P ∨ Q) ∨ A) → ¬C) replace proposition variable B by ¬¬(P ∨ Q) ∨ A in 41
43 (((P ∨ Q) ∨ A) → (¬¬(P ∨ Q) ∨ A)) → (¬(¬¬(P ∨ Q) ∨ A) → ¬((P ∨ Q) ∨ A)) replace proposition variable C by (P ∨ Q) ∨ A in 42
44 ¬(¬¬(P ∨ Q) ∨ A) → ¬((P ∨ Q) ∨ A) modus ponens with 39, 43
45 (P → Q) → (¬P ∨ Q) add proposition defimpl1
46 (¬P ∨ Q) → (P → Q) add proposition defimpl2
47 (C → ¬((P ∨ Q) ∨ A)) → (¬¬((P ∨ Q) ∨ A) → ¬C) replace proposition variable B by ¬((P ∨ Q) ∨ A) in 41
48 (¬(¬¬(P ∨ Q) ∨ A) → ¬((P ∨ Q) ∨ A)) → (¬¬((P ∨ Q) ∨ A) → ¬¬(¬¬(P ∨ Q) ∨ A)) replace proposition variable C by ¬(¬¬(P ∨ Q) ∨ A) in 47
49 ¬¬((P ∨ Q) ∨ A) → ¬¬(¬¬(P ∨ Q) ∨ A) modus ponens with 44, 48
50 (D → C) → ((¬(P ∨ (Q ∨ A)) ∨ D) → (¬(P ∨ (Q ∨ A)) ∨ C)) replace proposition variable B by ¬(P ∨ (Q ∨ A)) in 14
51 (D → ¬¬(¬¬(P ∨ Q) ∨ A)) → ((¬(P ∨ (Q ∨ A)) ∨ D) → (¬(P ∨ (Q ∨ A)) ∨ ¬¬(¬¬(P ∨ Q) ∨ A))) replace proposition variable C by ¬¬(¬¬(P ∨ Q) ∨ A) in 50
52 (¬¬((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 51
53 (¬(P ∨ (Q ∨ A)) ∨ ¬¬((P ∨ Q) ∨ A)) → (¬(P ∨ (Q ∨ A)) ∨ ¬¬(¬¬(P ∨ Q) ∨ A)) modus ponens with 49, 52
54 (C ∨ ¬¬(¬¬(P ∨ Q) ∨ A)) → (¬¬(¬¬(P ∨ Q) ∨ A) ∨ C) replace proposition variable B by ¬¬(¬¬(P ∨ Q) ∨ A) in 21
55 (¬(P ∨ (Q ∨ A)) ∨ ¬¬(¬¬(P ∨ Q) ∨ A)) → (¬¬(¬¬(P ∨ Q) ∨ A) ∨ ¬(P ∨ (Q ∨ A))) replace proposition variable C by ¬(P ∨ (Q ∨ A)) in 54
56 (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 27
57 (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 56
58 ((¬(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 57
59 ((¬(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 55, 58
60 (¬(P ∨ (Q ∨ A)) ∨ ¬¬((P ∨ Q) ∨ A)) → (¬¬(¬¬(P ∨ Q) ∨ A) ∨ ¬(P ∨ (Q ∨ A))) modus ponens with 53, 59
61 (C ∨ ¬(P ∨ (Q ∨ A))) → (¬(P ∨ (Q ∨ A)) ∨ C) replace proposition variable B by ¬(P ∨ (Q ∨ A)) in 21
62 (¬¬((P ∨ Q) ∨ A) ∨ ¬(P ∨ (Q ∨ A))) → (¬(P ∨ (Q ∨ A)) ∨ ¬¬((P ∨ Q) ∨ A)) replace proposition variable C by ¬¬((P ∨ Q) ∨ A) in 61
63 (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 27
64 (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 63
65 ((¬(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 64
66 ((¬¬((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 60, 65
67 (¬¬((P ∨ Q) ∨ A) ∨ ¬(P ∨ (Q ∨ A))) → (¬¬(¬¬(P ∨ Q) ∨ A) ∨ ¬(P ∨ (Q ∨ A))) modus ponens with 62, 66
68 (P → B) → (¬P ∨ B) replace proposition variable Q by B in 45
69 (C → B) → (¬C ∨ B) replace proposition variable P by C in 68
70 (C → ¬(P ∨ (Q ∨ A))) → (¬C ∨ ¬(P ∨ (Q ∨ A))) replace proposition variable B by ¬(P ∨ (Q ∨ A)) in 69
71 (¬((P ∨ Q) ∨ A) → ¬(P ∨ (Q ∨ A))) → (¬¬((P ∨ Q) ∨ A) ∨ ¬(P ∨ (Q ∨ A))) replace proposition variable C by ¬((P ∨ Q) ∨ A) in 70
72 (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 27
73 (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 72
74 ((¬¬((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 73
75 ((¬((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 67, 74
76 (¬((P ∨ Q) ∨ A) → ¬(P ∨ (Q ∨ A))) → (¬¬(¬¬(P ∨ Q) ∨ A) ∨ ¬(P ∨ (Q ∨ A))) modus ponens with 71, 75
77 (¬P ∨ B) → (P → B) replace proposition variable Q by B in 46
78 (¬C ∨ B) → (C → B) replace proposition variable P by C in 77
79 (¬C ∨ ¬(P ∨ (Q ∨ A))) → (C → ¬(P ∨ (Q ∨ A))) replace proposition variable B by ¬(P ∨ (Q ∨ A)) in 78
80 (¬¬(¬¬(P ∨ Q) ∨ A) ∨ ¬(P ∨ (Q ∨ A))) → (¬(¬¬(P ∨ Q) ∨ A) → ¬(P ∨ (Q ∨ A))) replace proposition variable C by ¬(¬¬(P ∨ Q) ∨ A) in 79
81 (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 72
82 ((¬¬(¬¬(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 81
83 ((¬((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 80, 82
84 (¬((P ∨ Q) ∨ A) → ¬(P ∨ (Q ∨ A))) → (¬(¬¬(P ∨ Q) ∨ A) → ¬(P ∨ (Q ∨ A))) modus ponens with 76, 83
85 ¬(¬¬(P ∨ Q) ∨ A) → ¬(P ∨ (Q ∨ A)) modus ponens with 7, 84
86 ¬¬P → P add proposition hilb6
87 ¬¬B → B replace proposition variable P by B in 86
88 ¬¬(Q ∨ A) → (Q ∨ A) replace proposition variable B by Q ∨ A in 87
89 (D → C) → ((P ∨ D) → (P ∨ C)) replace proposition variable B by P in 14
90 (D → (Q ∨ A)) → ((P ∨ D) → (P ∨ (Q ∨ A))) replace proposition variable C by Q ∨ A in 89
91 (¬¬(Q ∨ A) → (Q ∨ A)) → ((P ∨ ¬¬(Q ∨ A)) → (P ∨ (Q ∨ A))) replace proposition variable D by ¬¬(Q ∨ A) in 90
92 (P ∨ ¬¬(Q ∨ A)) → (P ∨ (Q ∨ A)) modus ponens with 88, 91
93 (C → (P ∨ (Q ∨ A))) → (¬(P ∨ (Q ∨ A)) → ¬C) replace proposition variable B by P ∨ (Q ∨ A) in 41
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 70
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 27
102 (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 101
103 ((¬¬(¬¬(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 102
104 ((¬(¬¬(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 99, 103
105 (¬(¬¬(P ∨ Q) ∨ A) → ¬(P ∨ (Q ∨ A))) → (¬¬(¬¬(P ∨ Q) ∨ A) ∨ ¬(P ∨ ¬¬(Q ∨ A))) modus ponens with 100, 104
106 (¬C ∨ ¬(P ∨ ¬¬(Q ∨ A))) → (C → ¬(P ∨ ¬¬(Q ∨ A))) replace proposition variable B by ¬(P ∨ ¬¬(Q ∨ A)) in 78
107 (¬¬(¬¬(P ∨ Q) ∨ A) ∨ ¬(P ∨ ¬¬(Q ∨ A))) → (¬(¬¬(P ∨ Q) ∨ A) → ¬(P ∨ ¬¬(Q ∨ A))) replace proposition variable C by ¬(¬¬(P ∨ Q) ∨ A) in 106
108 (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 101
109 ((¬¬(¬¬(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 108
110 ((¬(¬¬(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 107, 109
111 (¬(¬¬(P ∨ Q) ∨ A) → ¬(P ∨ (Q ∨ A))) → (¬(¬¬(P ∨ Q) ∨ A) → ¬(P ∨ ¬¬(Q ∨ A))) modus ponens with 105, 110
112 ¬(¬¬(P ∨ Q) ∨ A) → ¬(P ∨ ¬¬(Q ∨ A)) modus ponens with 85, 111
113 ¬(¬¬(P ∨ Q) ∨ B) → ¬(P ∨ ¬¬(Q ∨ B)) replace proposition variable A by B in 112
114 ¬(¬¬(P ∨ C) ∨ B) → ¬(P ∨ ¬¬(C ∨ B)) replace proposition variable Q by C in 113
115 ¬(¬¬(D ∨ C) ∨ B) → ¬(D ∨ ¬¬(C ∨ B)) replace proposition variable P by D in 114
116 ¬(¬¬(D ∨ C) ∨ ¬A) → ¬(D ∨ ¬¬(C ∨ ¬A)) replace proposition variable B by ¬A in 115
117 ¬(¬¬(D ∨ ¬Q) ∨ ¬A) → ¬(D ∨ ¬¬(¬Q ∨ ¬A)) replace proposition variable C by ¬Q in 116
118 ¬(¬¬(¬P ∨ ¬Q) ∨ ¬A) → ¬(¬P ∨ ¬¬(¬Q ∨ ¬A)) replace proposition variable D by ¬P in 117
119 (¬(¬P ∨ ¬Q) ∧ A) → ¬(¬P ∨ ¬¬(¬Q ∨ ¬A)) reverse abbreviation and in 118 at occurence 1
120 ((P ∧ Q) ∧ A) → ¬(¬P ∨ ¬¬(¬Q ∨ ¬A)) reverse abbreviation and in 119 at occurence 1
121 ((P ∧ Q) ∧ A) → (P ∧ ¬(¬Q ∨ ¬A)) reverse abbreviation and in 120 at occurence 1
122 ((P ∧ Q) ∧ A) → (P ∧ (Q ∧ A)) reverse abbreviation and in 121 at occurence 1
qed

Form for the conjunction rule:

11. Proposition
      P → (Q → (P ∧ Q))     (hilb28)

Proof:
1 P ∨ ¬P add proposition hilb4
2 (¬P ∨ ¬Q) ∨ ¬(¬P ∨ ¬Q) replace proposition variable P by ¬P ∨ ¬Q in 1
3 ((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)) add proposition hilb15
4 ((P ∨ Q) ∨ B) → (P ∨ (Q ∨ B)) replace proposition variable A by B in 3
5 ((P ∨ C) ∨ B) → (P ∨ (C ∨ B)) replace proposition variable Q by C in 4
6 ((D ∨ C) ∨ B) → (D ∨ (C ∨ B)) replace proposition variable P by D in 5
7 ((D ∨ C) ∨ ¬(¬P ∨ ¬Q)) → (D ∨ (C ∨ ¬(¬P ∨ ¬Q))) replace proposition variable B by ¬(¬P ∨ ¬Q) in 6
8 ((D ∨ ¬Q) ∨ ¬(¬P ∨ ¬Q)) → (D ∨ (¬Q ∨ ¬(¬P ∨ ¬Q))) replace proposition variable C by ¬Q in 7
9 ((¬P ∨ ¬Q) ∨ ¬(¬P ∨ ¬Q)) → (¬P ∨ (¬Q ∨ ¬(¬P ∨ ¬Q))) replace proposition variable D by ¬P in 8
10 ¬P ∨ (¬Q ∨ ¬(¬P ∨ ¬Q)) modus ponens with 2, 9
11 P → (¬Q ∨ ¬(¬P ∨ ¬Q)) reverse abbreviation impl in 10 at occurence 1
12 P → (Q → ¬(¬P ∨ ¬Q)) reverse abbreviation impl in 11 at occurence 1
13 P → (Q → (P ∧ Q)) reverse abbreviation and in 12 at occurence 1
qed

Preconditions could be put together in a conjunction (first direction):

12. Proposition
      (P → (Q → A)) → ((P ∧ Q) → A)     (hilb29)

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

Preconditions could be put together in a conjunction (second direction):

13. Proposition
      ((P ∧ Q) → A) → (P → (Q → A))     (hilb30)

Proof:
1 P → P add proposition hilb2
2 Q → Q replace proposition variable P by Q in 1
3 (P → (Q → A)) → (P → (Q → A)) replace proposition variable Q by P → (Q → A) in 2
4 (¬P ∨ (Q → A)) → (P → (Q → A)) use abbreviation impl in 3 at occurence 2
5 (¬P ∨ (¬Q ∨ A)) → (P → (Q → A)) use abbreviation impl in 4 at occurence 2
6 ((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)) add proposition hilb15
7 ((P ∨ Q) ∨ B) → (P ∨ (Q ∨ B)) replace proposition variable A by B in 6
8 ((P ∨ C) ∨ B) → (P ∨ (C ∨ B)) replace proposition variable Q by C in 7
9 ((D ∨ C) ∨ B) → (D ∨ (C ∨ B)) replace proposition variable P by D in 8
10 ((D ∨ C) ∨ A) → (D ∨ (C ∨ A)) replace proposition variable B by A in 9
11 ((D ∨ ¬Q) ∨ A) → (D ∨ (¬Q ∨ A)) replace proposition variable C by ¬Q in 10
12 ((¬P ∨ ¬Q) ∨ A) → (¬P ∨ (¬Q ∨ A)) replace proposition variable D by ¬P in 11
13 (P → Q) → (¬P ∨ Q) add proposition defimpl1
14 (¬P ∨ Q) → (P → Q) add proposition defimpl2
15 (P → Q) → (¬Q → ¬P) add proposition hilb7
16 (P → B) → (¬B → ¬P) replace proposition variable Q by B in 15
17 (C → B) → (¬B → ¬C) replace proposition variable P by C in 16
18 (C → (¬P ∨ (¬Q ∨ A))) → (¬(¬P ∨ (¬Q ∨ A)) → ¬C) replace proposition variable B by ¬P ∨ (¬Q ∨ A) in 17
19 (((¬P ∨ ¬Q) ∨ A) → (¬P ∨ (¬Q ∨ A))) → (¬(¬P ∨ (¬Q ∨ A)) → ¬((¬P ∨ ¬Q) ∨ A)) replace proposition variable C by (¬P ∨ ¬Q) ∨ A in 18
20 ¬(¬P ∨ (¬Q ∨ A)) → ¬((¬P ∨ ¬Q) ∨ A) modus ponens with 12, 19
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) → (((P → (Q → A)) ∨ D) → ((P → (Q → A)) ∨ C)) replace proposition variable B by P → (Q → A) in 24
26 (D → ¬((¬P ∨ ¬Q) ∨ A)) → (((P → (Q → A)) ∨ D) → ((P → (Q → A)) ∨ ¬((¬P ∨ ¬Q) ∨ A))) replace proposition variable C by ¬((¬P ∨ ¬Q) ∨ A) in 25
27 (¬(¬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 26
28 ((P → (Q → A)) ∨ ¬(¬P ∨ (¬Q ∨ A))) → ((P → (Q → A)) ∨ ¬((¬P ∨ ¬Q) ∨ A)) modus ponens with 20, 27
29 (P ∨ Q) → (Q ∨ P) add axiom axiom3
30 (P ∨ B) → (B ∨ P) replace proposition variable Q by B in 29
31 (C ∨ B) → (B ∨ C) replace proposition variable P by C in 30
32 (C ∨ ¬((¬P ∨ ¬Q) ∨ A)) → (¬((¬P ∨ ¬Q) ∨ A) ∨ C) replace proposition variable B by ¬((¬P ∨ ¬Q) ∨ A) in 31
33 ((P → (Q → A)) ∨ ¬((¬P ∨ ¬Q) ∨ A)) → (¬((¬P ∨ ¬Q) ∨ A) ∨ (P → (Q → A))) replace proposition variable C by P → (Q → A) in 32
34 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
35 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 34
36 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 35
37 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 36
38 (D → C) → ((((P → (Q → A)) ∨ ¬(¬P ∨ (¬Q ∨ A))) → D) → (((P → (Q → A)) ∨ ¬(¬P ∨ (¬Q ∨ A))) → C)) replace proposition variable B by (P → (Q → A)) ∨ ¬(¬P ∨ (¬Q ∨ A)) in 37
39 (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 38
40 (((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 39
41 (((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 33, 40
42 ((P → (Q → A)) ∨ ¬(¬P ∨ (¬Q ∨ A))) → (¬((¬P ∨ ¬Q) ∨ A) ∨ (P → (Q → A))) modus ponens with 28, 41
43 (C ∨ (P → (Q → A))) → ((P → (Q → A)) ∨ C) replace proposition variable B by P → (Q → A) in 31
44 (¬(¬P ∨ (¬Q ∨ A)) ∨ (P → (Q → A))) → ((P → (Q → A)) ∨ ¬(¬P ∨ (¬Q ∨ A))) replace proposition variable C by ¬(¬P ∨ (¬Q ∨ A)) in 43
45 (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 37
46 (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 45
47 (((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 46
48 ((¬(¬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 42, 47
49 (¬(¬P ∨ (¬Q ∨ A)) ∨ (P → (Q → A))) → (¬((¬P ∨ ¬Q) ∨ A) ∨ (P → (Q → A))) modus ponens with 44, 48
50 (P → B) → (¬P ∨ B) replace proposition variable Q by B in 13
51 (C → B) → (¬C ∨ B) replace proposition variable P by C in 50
52 (C → (P → (Q → A))) → (¬C ∨ (P → (Q → A))) replace proposition variable B by P → (Q → A) in 51
53 ((¬P ∨ (¬Q ∨ A)) → (P → (Q → A))) → (¬(¬P ∨ (¬Q ∨ A)) ∨ (P → (Q → A))) replace proposition variable C by ¬P ∨ (¬Q ∨ A) in 52
54 (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 37
55 (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 54
56 ((¬(¬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 55
57 (((¬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 49, 56
58 ((¬P ∨ (¬Q ∨ A)) → (P → (Q → A))) → (¬((¬P ∨ ¬Q) ∨ A) ∨ (P → (Q → A))) modus ponens with 53, 57
59 (¬P ∨ B) → (P → B) replace proposition variable Q by B in 14
60 (¬C ∨ B) → (C → B) replace proposition variable P by C in 59
61 (¬C ∨ (P → (Q → A))) → (C → (P → (Q → A))) replace proposition variable B by P → (Q → A) in 60
62 (¬((¬P ∨ ¬Q) ∨ A) ∨ (P → (Q → A))) → (((¬P ∨ ¬Q) ∨ A) → (P → (Q → A))) replace proposition variable C by (¬P ∨ ¬Q) ∨ A in 61
63 (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 54
64 ((¬((¬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 63
65 (((¬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 62, 64
66 ((¬P ∨ (¬Q ∨ A)) → (P → (Q → A))) → (((¬P ∨ ¬Q) ∨ A) → (P → (Q → A))) modus ponens with 58, 65
67 ((¬P ∨ ¬Q) ∨ A) → (P → (Q → A)) modus ponens with 5, 66
68 ¬¬P → P add proposition hilb6
69 ¬¬A → A replace proposition variable P by A in 68
70 ¬¬(¬P ∨ ¬Q) → (¬P ∨ ¬Q) replace proposition variable A by ¬P ∨ ¬Q in 69
71 (D → C) → ((A ∨ D) → (A ∨ C)) replace proposition variable B by A in 24
72 (D → (¬P ∨ ¬Q)) → ((A ∨ D) → (A ∨ (¬P ∨ ¬Q))) replace proposition variable C by ¬P ∨ ¬Q in 71
73 (¬¬(¬P ∨ ¬Q) → (¬P ∨ ¬Q)) → ((A ∨ ¬¬(¬P ∨ ¬Q)) → (A ∨ (¬P ∨ ¬Q))) replace proposition variable D by ¬¬(¬P ∨ ¬Q) in 72
74 (A ∨ ¬¬(¬P ∨ ¬Q)) → (A ∨ (¬P ∨ ¬Q)) modus ponens with 70, 73
75 (C ∨ (¬P ∨ ¬Q)) → ((¬P ∨ ¬Q) ∨ C) replace proposition variable B by ¬P ∨ ¬Q in 31
76 (A ∨ (¬P ∨ ¬Q)) → ((¬P ∨ ¬Q) ∨ A) replace proposition variable C by A in 75
77 (D → C) → (((A ∨ ¬¬(¬P ∨ ¬Q)) → D) → ((A ∨ ¬¬(¬P ∨ ¬Q)) → C)) replace proposition variable B by A ∨ ¬¬(¬P ∨ ¬Q) in 37
78 (D → ((¬P ∨ ¬Q) ∨ A)) → (((A ∨ ¬¬(¬P ∨ ¬Q)) → D) → ((A ∨ ¬¬(¬P ∨ ¬Q)) → ((¬P ∨ ¬Q) ∨ A))) replace proposition variable C by (¬P ∨ ¬Q) ∨ A in 77
79 ((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 78
80 ((A ∨ ¬¬(¬P ∨ ¬Q)) → (A ∨ (¬P ∨ ¬Q))) → ((A ∨ ¬¬(¬P ∨ ¬Q)) → ((¬P ∨ ¬Q) ∨ A)) modus ponens with 76, 79
81 (A ∨ ¬¬(¬P ∨ ¬Q)) → ((¬P ∨ ¬Q) ∨ A) modus ponens with 74, 80
82 (C ∨ A) → (A ∨ C) replace proposition variable B by A in 31
83 (¬¬(¬P ∨ ¬Q) ∨ A) → (A ∨ ¬¬(¬P ∨ ¬Q)) replace proposition variable C by ¬¬(¬P ∨ ¬Q) in 82
84 (D → C) → (((¬¬(¬P ∨ ¬Q) ∨ A) → D) → ((¬¬(¬P ∨ ¬Q) ∨ A) → C)) replace proposition variable B by ¬¬(¬P ∨ ¬Q) ∨ A in 37
85 (D → ((¬P ∨ ¬Q) ∨ A)) → (((¬¬(¬P ∨ ¬Q) ∨ A) → D) → ((¬¬(¬P ∨ ¬Q) ∨ A) → ((¬P ∨ ¬Q) ∨ A))) replace proposition variable C by (¬P ∨ ¬Q) ∨ A in 84
86 ((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 85
87 ((¬¬(¬P ∨ ¬Q) ∨ A) → (A ∨ ¬¬(¬P ∨ ¬Q))) → ((¬¬(¬P ∨ ¬Q) ∨ A) → ((¬P ∨ ¬Q) ∨ A)) modus ponens with 81, 86
88 (¬¬(¬P ∨ ¬Q) ∨ A) → ((¬P ∨ ¬Q) ∨ A) modus ponens with 83, 87
89 (C → ((¬P ∨ ¬Q) ∨ A)) → (¬((¬P ∨ ¬Q) ∨ A) → ¬C) replace proposition variable B by (¬P ∨ ¬Q) ∨ A in 17
90 ((¬¬(¬P ∨ ¬Q) ∨ A) → ((¬P ∨ ¬Q) ∨ A)) → (¬((¬P ∨ ¬Q) ∨ A) → ¬(¬¬(¬P ∨ ¬Q) ∨ A)) replace proposition variable C by ¬¬(¬P ∨ ¬Q) ∨ A in 89
91 ¬((¬P ∨ ¬Q) ∨ A) → ¬(¬¬(¬P ∨ ¬Q) ∨ A) modus ponens with 88, 90
92 (D → ¬(¬¬(¬P ∨ ¬Q) ∨ A)) → (((P → (Q → A)) ∨ D) → ((P → (Q → A)) ∨ ¬(¬¬(¬P ∨ ¬Q) ∨ A))) replace proposition variable C by ¬(¬¬(¬P ∨ ¬Q) ∨ A) in 25
93 (¬((¬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 92
94 ((P → (Q → A)) ∨ ¬((¬P ∨ ¬Q) ∨ A)) → ((P → (Q → A)) ∨ ¬(¬¬(¬P ∨ ¬Q) ∨ A)) modus ponens with 91, 93
95 (C ∨ ¬(¬¬(¬P ∨ ¬Q) ∨ A)) → (¬(¬¬(¬P ∨ ¬Q) ∨ A) ∨ C) replace proposition variable B by ¬(¬¬(¬P ∨ ¬Q) ∨ A) in 31
96 ((P → (Q → A)) ∨ ¬(¬¬(¬P ∨ ¬Q) ∨ A)) → (¬(¬¬(¬P ∨ ¬Q) ∨ A) ∨ (P → (Q → A))) replace proposition variable C by P → (Q → A) in 95
97 (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 37
98 (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 97
99 (((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 98
100 (((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 96, 99
101 ((P → (Q → A)) ∨ ¬((¬P ∨ ¬Q) ∨ A)) → (¬(¬¬(¬P ∨ ¬Q) ∨ A) ∨ (P → (Q → A))) modus ponens with 94, 100
102 (¬((¬P ∨ ¬Q) ∨ A) ∨ (P → (Q → A))) → ((P → (Q → A)) ∨ ¬((¬P ∨ ¬Q) ∨ A)) replace proposition variable C by ¬((¬P ∨ ¬Q) ∨ A) in 43
103 (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 37
104 (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 103
105 (((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 104
106 ((¬((¬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 101, 105
107 (¬((¬P ∨ ¬Q) ∨ A) ∨ (P → (Q → A))) → (¬(¬¬(¬P ∨ ¬Q) ∨ A) ∨ (P → (Q → A))) modus ponens with 102, 106
108 (((¬P ∨ ¬Q) ∨ A) → (P → (Q → A))) → (¬((¬P ∨ ¬Q) ∨ A) ∨ (P → (Q → A))) replace proposition variable C by (¬P ∨ ¬Q) ∨ A in 52
109 (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 37
110 (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 109
111 ((¬((¬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 110
112 ((((¬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 107, 111
113 (((¬P ∨ ¬Q) ∨ A) → (P → (Q → A))) → (¬(¬¬(¬P ∨ ¬Q) ∨ A) ∨ (P → (Q → A))) modus ponens with 108, 112
114 (¬(¬¬(¬P ∨ ¬Q) ∨ A) ∨ (P → (Q → A))) → ((¬¬(¬P ∨ ¬Q) ∨ A) → (P → (Q → A))) replace proposition variable C by ¬¬(¬P ∨ ¬Q) ∨ A in 61
115 (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 109
116 ((¬(¬¬(¬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 115
117 ((((¬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 114, 116
118 (((¬P ∨ ¬Q) ∨ A) → (P → (Q → A))) → ((¬¬(¬P ∨ ¬Q) ∨ A) → (P → (Q → A))) modus ponens with 113, 117
119 (¬¬(¬P ∨ ¬Q) ∨ A) → (P → (Q → A)) modus ponens with 67, 118
120 (¬(¬P ∨ ¬Q) → A) → (P → (Q → A)) reverse abbreviation impl in 119 at occurence 1
121 ((P ∧ Q) → A) → (P → (Q → A)) reverse abbreviation and in 120 at occurence 1
qed

Absorbtion of a conjunction (first direction):

14. Proposition
      (P ∧ P) → P     (hilb31)

Proof:
1 (P ∧ Q) → P add proposition hilb24
2 (P ∧ P) → P replace proposition variable Q by P in 1
qed

Absorbtion of a conjunction (second direction):

15. Proposition
      P → (P ∧ P)     (hilb32)

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

Absorbtion of identical preconditions (first direction):

16. Proposition
      (P → (P → Q)) → (P → Q)     (hilb33)

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

Absorbtion of identical preconditions (second direction):

17. Proposition
      (P → Q) → (P → (P → Q))     (hilb34)

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

Cross References

This document is used by the following documents: