for questions or link request: module admin

Further Theorems of Propositional Calculus

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

Description

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

References

This document uses the results of the following documents:

Content

First distributive law (first direction):

1. Proposition
      (P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A))     (hilb36)

Proof:
1 (P ∧ Q) → P add proposition hilb24
2 (P ∧ A) → P replace proposition variable Q by A in 1
3 (B ∧ A) → B replace proposition variable P by B in 2
4 (Q ∧ A) → Q replace proposition variable B by Q in 3
5 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
6 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 5
7 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 6
8 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 7
9 (D → C) → ((P ∨ D) → (P ∨ C)) replace proposition variable B by P in 8
10 (D → Q) → ((P ∨ D) → (P ∨ Q)) replace proposition variable C by Q in 9
11 ((Q ∧ A) → Q) → ((P ∨ (Q ∧ A)) → (P ∨ Q)) replace proposition variable D by Q ∧ A in 10
12 (P ∨ (Q ∧ A)) → (P ∨ Q) modus ponens with 4, 11
13 (P ∧ Q) → Q add proposition hilb25
14 (P ∧ A) → A replace proposition variable Q by A in 13
15 (B ∧ A) → A replace proposition variable P by B in 14
16 (Q ∧ A) → A replace proposition variable B by Q in 15
17 (D → A) → ((P ∨ D) → (P ∨ A)) replace proposition variable C by A in 9
18 ((Q ∧ A) → A) → ((P ∨ (Q ∧ A)) → (P ∨ A)) replace proposition variable D by Q ∧ A in 17
19 (P ∨ (Q ∧ A)) → (P ∨ A) modus ponens with 16, 18
20 P → (Q → (P ∧ Q)) add proposition hilb28
21 P → (A → (P ∧ A)) replace proposition variable Q by A in 20
22 B → (A → (B ∧ A)) replace proposition variable P by B in 21
23 B → ((P ∨ A) → (B ∧ (P ∨ A))) replace proposition variable A by P ∨ A in 22
24 (P ∨ Q) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A))) replace proposition variable B by P ∨ Q in 23
25 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
26 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 25
27 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 26
28 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 27
29 (D → C) → (((P ∨ (Q ∧ A)) → D) → ((P ∨ (Q ∧ A)) → C)) replace proposition variable B by P ∨ (Q ∧ A) in 28
30 (D → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A)))) → (((P ∨ (Q ∧ A)) → D) → ((P ∨ (Q ∧ A)) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A))))) replace proposition variable C by (P ∨ A) → ((P ∨ Q) ∧ (P ∨ A)) in 29
31 ((P ∨ Q) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A)))) → (((P ∨ (Q ∧ A)) → (P ∨ Q)) → ((P ∨ (Q ∧ A)) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A))))) replace proposition variable D by P ∨ Q in 30
32 ((P ∨ (Q ∧ A)) → (P ∨ Q)) → ((P ∨ (Q ∧ A)) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A)))) modus ponens with 24, 31
33 (P ∨ (Q ∧ A)) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A))) modus ponens with 12, 32
34 (P → (Q → A)) → (Q → (P → A)) add proposition hilb16
35 (P → (Q → B)) → (Q → (P → B)) replace proposition variable A by B in 34
36 (P → (C → B)) → (C → (P → B)) replace proposition variable Q by C in 35
37 (D → (C → B)) → (C → (D → B)) replace proposition variable P by D in 36
38 (D → (C → ((P ∨ Q) ∧ (P ∨ A)))) → (C → (D → ((P ∨ Q) ∧ (P ∨ A)))) replace proposition variable B by (P ∨ Q) ∧ (P ∨ A) in 37
39 (D → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A)))) → ((P ∨ A) → (D → ((P ∨ Q) ∧ (P ∨ A)))) replace proposition variable C by P ∨ A in 38
40 ((P ∨ (Q ∧ A)) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A)))) → ((P ∨ A) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)))) replace proposition variable D by P ∨ (Q ∧ A) in 39
41 (P ∨ A) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A))) modus ponens with 33, 40
42 (D → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)))) → (((P ∨ (Q ∧ A)) → D) → ((P ∨ (Q ∧ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A))))) replace proposition variable C by (P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)) in 29
43 ((P ∨ A) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)))) → (((P ∨ (Q ∧ A)) → (P ∨ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A))))) replace proposition variable D by P ∨ A in 42
44 ((P ∨ (Q ∧ A)) → (P ∨ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)))) modus ponens with 41, 43
45 (P ∨ (Q ∧ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A))) modus ponens with 19, 44
46 (P → (P → Q)) → (P → Q) add proposition hilb33
47 (P → (P → A)) → (P → A) replace proposition variable Q by A in 46
48 (B → (B → A)) → (B → A) replace proposition variable P by B in 47
49 (B → (B → ((P ∨ Q) ∧ (P ∨ A)))) → (B → ((P ∨ Q) ∧ (P ∨ A))) replace proposition variable A by (P ∨ Q) ∧ (P ∨ A) in 48
50 ((P ∨ (Q ∧ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)))) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A))) replace proposition variable B by P ∨ (Q ∧ A) in 49
51 (P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)) modus ponens with 45, 50
qed

First distributive law (second direction):

2. Proposition
      ((P ∨ Q) ∧ (P ∨ A)) → (P ∨ (Q ∧ A))     (hilb37)

Proof:
1 P → (Q → (P ∧ Q)) add proposition hilb28
2 P → (A → (P ∧ A)) replace proposition variable Q by A in 1
3 B → (A → (B ∧ A)) replace proposition variable P by B in 2
4 Q → (A → (Q ∧ A)) replace proposition variable B by Q in 3
5 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
6 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 5
7 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 6
8 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 7
9 (D → C) → ((P ∨ D) → (P ∨ C)) replace proposition variable B by P in 8
10 (D → (Q ∧ A)) → ((P ∨ D) → (P ∨ (Q ∧ A))) replace proposition variable C by Q ∧ A in 9
11 (A → (Q ∧ A)) → ((P ∨ A) → (P ∨ (Q ∧ A))) replace proposition variable D by A in 10
12 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
13 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 12
14 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 13
15 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 14
16 (D → C) → ((Q → D) → (Q → C)) replace proposition variable B by Q in 15
17 (D → ((P ∨ A) → (P ∨ (Q ∧ A)))) → ((Q → D) → (Q → ((P ∨ A) → (P ∨ (Q ∧ A))))) replace proposition variable C by (P ∨ A) → (P ∨ (Q ∧ A)) in 16
18 ((A → (Q ∧ A)) → ((P ∨ A) → (P ∨ (Q ∧ A)))) → ((Q → (A → (Q ∧ A))) → (Q → ((P ∨ A) → (P ∨ (Q ∧ A))))) replace proposition variable D by A → (Q ∧ A) in 17
19 (Q → (A → (Q ∧ A))) → (Q → ((P ∨ A) → (P ∨ (Q ∧ A)))) modus ponens with 11, 18
20 Q → ((P ∨ A) → (P ∨ (Q ∧ A))) modus ponens with 4, 19
21 (P → (Q → A)) → (Q → (P → A)) add proposition hilb16
22 (P → (Q → B)) → (Q → (P → B)) replace proposition variable A by B in 21
23 (P → (C → B)) → (C → (P → B)) replace proposition variable Q by C in 22
24 (D → (C → B)) → (C → (D → B)) replace proposition variable P by D in 23
25 (D → (C → (P ∨ (Q ∧ A)))) → (C → (D → (P ∨ (Q ∧ A)))) replace proposition variable B by P ∨ (Q ∧ A) in 24
26 (D → ((P ∨ A) → (P ∨ (Q ∧ A)))) → ((P ∨ A) → (D → (P ∨ (Q ∧ A)))) replace proposition variable C by P ∨ A in 25
27 (Q → ((P ∨ A) → (P ∨ (Q ∧ A)))) → ((P ∨ A) → (Q → (P ∨ (Q ∧ A)))) replace proposition variable D by Q in 26
28 (P ∨ A) → (Q → (P ∨ (Q ∧ A))) modus ponens with 20, 27
29 (D → (P ∨ (Q ∧ A))) → ((P ∨ D) → (P ∨ (P ∨ (Q ∧ A)))) replace proposition variable C by P ∨ (Q ∧ A) in 9
30 (Q → (P ∨ (Q ∧ A))) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) replace proposition variable D by Q in 29
31 (D → C) → (((P ∨ A) → D) → ((P ∨ A) → C)) replace proposition variable B by P ∨ A in 15
32 (D → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (((P ∨ A) → D) → ((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))))) replace proposition variable C by (P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))) in 31
33 ((Q → (P ∨ (Q ∧ A))) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (((P ∨ A) → (Q → (P ∨ (Q ∧ A)))) → ((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))))) replace proposition variable D by Q → (P ∨ (Q ∧ A)) in 32
34 ((P ∨ A) → (Q → (P ∨ (Q ∧ A)))) → ((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) modus ponens with 30, 33
35 (P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) modus ponens with 28, 34
36 (P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A) add proposition hilb14
37 (P ∨ (Q ∨ B)) → ((P ∨ Q) ∨ B) replace proposition variable A by B in 36
38 (P ∨ (C ∨ B)) → ((P ∨ C) ∨ B) replace proposition variable Q by C in 37
39 (D ∨ (C ∨ B)) → ((D ∨ C) ∨ B) replace proposition variable P by D in 38
40 (D ∨ (C ∨ (Q ∧ A))) → ((D ∨ C) ∨ (Q ∧ A)) replace proposition variable B by Q ∧ A in 39
41 (D ∨ (P ∨ (Q ∧ A))) → ((D ∨ P) ∨ (Q ∧ A)) replace proposition variable C by P in 40
42 (P ∨ (P ∨ (Q ∧ A))) → ((P ∨ P) ∨ (Q ∧ A)) replace proposition variable D by P in 41
43 (P → Q) → (¬P ∨ Q) add proposition defimpl1
44 (¬P ∨ Q) → (P → Q) add proposition defimpl2
45 (D → C) → ((¬(P ∨ Q) ∨ D) → (¬(P ∨ Q) ∨ C)) replace proposition variable B by ¬(P ∨ Q) in 8
46 (D → ((P ∨ P) ∨ (Q ∧ A))) → ((¬(P ∨ Q) ∨ D) → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A)))) replace proposition variable C by (P ∨ P) ∨ (Q ∧ A) in 45
47 ((P ∨ (P ∨ (Q ∧ A))) → ((P ∨ P) ∨ (Q ∧ A))) → ((¬(P ∨ Q) ∨ (P ∨ (P ∨ (Q ∧ A)))) → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A)))) replace proposition variable D by P ∨ (P ∨ (Q ∧ A)) in 46
48 (¬(P ∨ Q) ∨ (P ∨ (P ∨ (Q ∧ A)))) → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A))) modus ponens with 42, 47
49 (P → B) → (¬P ∨ B) replace proposition variable Q by B in 43
50 (C → B) → (¬C ∨ B) replace proposition variable P by C in 49
51 (C → (P ∨ (P ∨ (Q ∧ A)))) → (¬C ∨ (P ∨ (P ∨ (Q ∧ A)))) replace proposition variable B by P ∨ (P ∨ (Q ∧ A)) in 50
52 ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → (¬(P ∨ Q) ∨ (P ∨ (P ∨ (Q ∧ A)))) replace proposition variable C by P ∨ Q in 51
53 (D → C) → ((((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → D) → (((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → C)) replace proposition variable B by (P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))) in 15
54 (D → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A)))) → ((((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → D) → (((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A))))) replace proposition variable C by ¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A)) in 53
55 ((¬(P ∨ Q) ∨ (P ∨ (P ∨ (Q ∧ A)))) → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A)))) → ((((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → (¬(P ∨ Q) ∨ (P ∨ (P ∨ (Q ∧ A))))) → (((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A))))) replace proposition variable D by ¬(P ∨ Q) ∨ (P ∨ (P ∨ (Q ∧ A))) in 54
56 (((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → (¬(P ∨ Q) ∨ (P ∨ (P ∨ (Q ∧ A))))) → (((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A)))) modus ponens with 48, 55
57 ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A))) modus ponens with 52, 56
58 (¬P ∨ B) → (P → B) replace proposition variable Q by B in 44
59 (¬C ∨ B) → (C → B) replace proposition variable P by C in 58
60 (¬C ∨ ((P ∨ P) ∨ (Q ∧ A))) → (C → ((P ∨ P) ∨ (Q ∧ A))) replace proposition variable B by (P ∨ P) ∨ (Q ∧ A) in 59
61 (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A))) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) replace proposition variable C by P ∨ Q in 60
62 (D → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → ((((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → D) → (((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) replace proposition variable C by (P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)) in 53
63 ((¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A))) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → ((((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A)))) → (((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) replace proposition variable D by ¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A)) in 62
64 (((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A)))) → (((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) modus ponens with 61, 63
65 ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) modus ponens with 57, 64
66 (D → C) → ((¬(P ∨ A) ∨ D) → (¬(P ∨ A) ∨ C)) replace proposition variable B by ¬(P ∨ A) in 8
67 (D → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → ((¬(P ∨ A) ∨ D) → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) replace proposition variable C by (P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)) in 66
68 (((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → ((¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) replace proposition variable D by (P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))) in 67
69 (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) modus ponens with 65, 68
70 (C → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (¬C ∨ ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) replace proposition variable B by (P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))) in 50
71 ((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) replace proposition variable C by P ∨ A in 70
72 (D → C) → ((((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → D) → (((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → C)) replace proposition variable B by (P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) in 15
73 (D → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) → ((((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → D) → (((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))))) replace proposition variable C by ¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) in 72
74 ((¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) → ((((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))))) → (((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))))) replace proposition variable D by ¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) in 73
75 (((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))))) → (((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) modus ponens with 69, 74
76 ((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) modus ponens with 71, 75
77 (¬C ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (C → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) replace proposition variable B by (P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)) in 59
78 (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → ((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) replace proposition variable C by P ∨ A in 77
79 (D → ((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) → ((((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → D) → (((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → ((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))))) replace proposition variable C by (P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) in 72
80 ((¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → ((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) → ((((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) → (((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → ((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))))) replace proposition variable D by ¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) in 79
81 (((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) → (((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → ((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) modus ponens with 78, 80
82 ((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → ((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) modus ponens with 76, 81
83 (P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) modus ponens with 35, 82
84 (P ∨ P) → P add proposition hilb11
85 (D → C) → (((Q ∧ A) ∨ D) → ((Q ∧ A) ∨ C)) replace proposition variable B by Q ∧ A in 8
86 (D → P) → (((Q ∧ A) ∨ D) → ((Q ∧ A) ∨ P)) replace proposition variable C by P in 85
87 ((P ∨ P) → P) → (((Q ∧ A) ∨ (P ∨ P)) → ((Q ∧ A) ∨ P)) replace proposition variable D by P ∨ P in 86
88 ((Q ∧ A) ∨ (P ∨ P)) → ((Q ∧ A) ∨ P) modus ponens with 84, 87
89 (P ∨ Q) → (Q ∨ P) add axiom axiom3
90 (P ∨ B) → (B ∨ P) replace proposition variable Q by B in 89
91 (C ∨ B) → (B ∨ C) replace proposition variable P by C in 90
92 (C ∨ P) → (P ∨ C) replace proposition variable B by P in 91
93 ((Q ∧ A) ∨ P) → (P ∨ (Q ∧ A)) replace proposition variable C by Q ∧ A in 92
94 (D → C) → ((((Q ∧ A) ∨ (P ∨ P)) → D) → (((Q ∧ A) ∨ (P ∨ P)) → C)) replace proposition variable B by (Q ∧ A) ∨ (P ∨ P) in 15
95 (D → (P ∨ (Q ∧ A))) → ((((Q ∧ A) ∨ (P ∨ P)) → D) → (((Q ∧ A) ∨ (P ∨ P)) → (P ∨ (Q ∧ A)))) replace proposition variable C by P ∨ (Q ∧ A) in 94
96 (((Q ∧ A) ∨ P) → (P ∨ (Q ∧ A))) → ((((Q ∧ A) ∨ (P ∨ P)) → ((Q ∧ A) ∨ P)) → (((Q ∧ A) ∨ (P ∨ P)) → (P ∨ (Q ∧ A)))) replace proposition variable D by (Q ∧ A) ∨ P in 95
97 (((Q ∧ A) ∨ (P ∨ P)) → ((Q ∧ A) ∨ P)) → (((Q ∧ A) ∨ (P ∨ P)) → (P ∨ (Q ∧ A))) modus ponens with 93, 96
98 ((Q ∧ A) ∨ (P ∨ P)) → (P ∨ (Q ∧ A)) modus ponens with 88, 97
99 (C ∨ (Q ∧ A)) → ((Q ∧ A) ∨ C) replace proposition variable B by Q ∧ A in 91
100 ((P ∨ P) ∨ (Q ∧ A)) → ((Q ∧ A) ∨ (P ∨ P)) replace proposition variable C by P ∨ P in 99
101 (D → C) → ((((P ∨ P) ∨ (Q ∧ A)) → D) → (((P ∨ P) ∨ (Q ∧ A)) → C)) replace proposition variable B by (P ∨ P) ∨ (Q ∧ A) in 15
102 (D → (P ∨ (Q ∧ A))) → ((((P ∨ P) ∨ (Q ∧ A)) → D) → (((P ∨ P) ∨ (Q ∧ A)) → (P ∨ (Q ∧ A)))) replace proposition variable C by P ∨ (Q ∧ A) in 101
103 (((Q ∧ A) ∨ (P ∨ P)) → (P ∨ (Q ∧ A))) → ((((P ∨ P) ∨ (Q ∧ A)) → ((Q ∧ A) ∨ (P ∨ P))) → (((P ∨ P) ∨ (Q ∧ A)) → (P ∨ (Q ∧ A)))) replace proposition variable D by (Q ∧ A) ∨ (P ∨ P) in 102
104 (((P ∨ P) ∨ (Q ∧ A)) → ((Q ∧ A) ∨ (P ∨ P))) → (((P ∨ P) ∨ (Q ∧ A)) → (P ∨ (Q ∧ A))) modus ponens with 98, 103
105 ((P ∨ P) ∨ (Q ∧ A)) → (P ∨ (Q ∧ A)) modus ponens with 100, 104
106 (D → (P ∨ (Q ∧ A))) → ((¬(P ∨ Q) ∨ D) → (¬(P ∨ Q) ∨ (P ∨ (Q ∧ A)))) replace proposition variable C by P ∨ (Q ∧ A) in 45
107 (((P ∨ P) ∨ (Q ∧ A)) → (P ∨ (Q ∧ A))) → ((¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A))) → (¬(P ∨ Q) ∨ (P ∨ (Q ∧ A)))) replace proposition variable D by (P ∨ P) ∨ (Q ∧ A) in 106
108 (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A))) → (¬(P ∨ Q) ∨ (P ∨ (Q ∧ A))) modus ponens with 105, 107
109 (C → ((P ∨ P) ∨ (Q ∧ A))) → (¬C ∨ ((P ∨ P) ∨ (Q ∧ A))) replace proposition variable B by (P ∨ P) ∨ (Q ∧ A) in 50
110 ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A))) replace proposition variable C by P ∨ Q in 109
111 (D → C) → ((((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → D) → (((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → C)) replace proposition variable B by (P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)) in 15
112 (D → (¬(P ∨ Q) ∨ (P ∨ (Q ∧ A)))) → ((((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → D) → (((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → (¬(P ∨ Q) ∨ (P ∨ (Q ∧ A))))) replace proposition variable C by ¬(P ∨ Q) ∨ (P ∨ (Q ∧ A)) in 111
113 ((¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A))) → (¬(P ∨ Q) ∨ (P ∨ (Q ∧ A)))) → ((((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A)))) → (((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → (¬(P ∨ Q) ∨ (P ∨ (Q ∧ A))))) replace proposition variable D by ¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A)) in 112
114 (((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → (¬(P ∨ Q) ∨ ((P ∨ P) ∨ (Q ∧ A)))) → (((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → (¬(P ∨ Q) ∨ (P ∨ (Q ∧ A)))) modus ponens with 108, 113
115 ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → (¬(P ∨ Q) ∨ (P ∨ (Q ∧ A))) modus ponens with 110, 114
116 (¬C ∨ (P ∨ (Q ∧ A))) → (C → (P ∨ (Q ∧ A))) replace proposition variable B by P ∨ (Q ∧ A) in 59
117 (¬(P ∨ Q) ∨ (P ∨ (Q ∧ A))) → ((P ∨ Q) → (P ∨ (Q ∧ A))) replace proposition variable C by P ∨ Q in 116
118 (D → ((P ∨ Q) → (P ∨ (Q ∧ A)))) → ((((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → D) → (((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → ((P ∨ Q) → (P ∨ (Q ∧ A))))) replace proposition variable C by (P ∨ Q) → (P ∨ (Q ∧ A)) in 111
119 ((¬(P ∨ Q) ∨ (P ∨ (Q ∧ A))) → ((P ∨ Q) → (P ∨ (Q ∧ A)))) → ((((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → (¬(P ∨ Q) ∨ (P ∨ (Q ∧ A)))) → (((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → ((P ∨ Q) → (P ∨ (Q ∧ A))))) replace proposition variable D by ¬(P ∨ Q) ∨ (P ∨ (Q ∧ A)) in 118
120 (((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → (¬(P ∨ Q) ∨ (P ∨ (Q ∧ A)))) → (((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → ((P ∨ Q) → (P ∨ (Q ∧ A)))) modus ponens with 117, 119
121 ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → ((P ∨ Q) → (P ∨ (Q ∧ A))) modus ponens with 115, 120
122 (D → ((P ∨ Q) → (P ∨ (Q ∧ A)))) → ((¬(P ∨ A) ∨ D) → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A))))) replace proposition variable C by (P ∨ Q) → (P ∨ (Q ∧ A)) in 66
123 (((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) → ((P ∨ Q) → (P ∨ (Q ∧ A)))) → ((¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A))))) replace proposition variable D by (P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)) in 122
124 (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A)))) modus ponens with 121, 123
125 (C → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (¬C ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) replace proposition variable B by (P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)) in 50
126 ((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) replace proposition variable C by P ∨ A in 125
127 (D → C) → ((((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → D) → (((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → C)) replace proposition variable B by (P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) in 15
128 (D → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A))))) → ((((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → D) → (((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A)))))) replace proposition variable C by ¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A))) in 127
129 ((¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A))))) → ((((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) → (((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A)))))) replace proposition variable D by ¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) in 128
130 (((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (¬(P ∨ A) ∨ ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))))) → (((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A))))) modus ponens with 124, 129
131 ((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A)))) modus ponens with 126, 130
132 (¬C ∨ ((P ∨ Q) → (P ∨ (Q ∧ A)))) → (C → ((P ∨ Q) → (P ∨ (Q ∧ A)))) replace proposition variable B by (P ∨ Q) → (P ∨ (Q ∧ A)) in 59
133 (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A)))) → ((P ∨ A) → ((P ∨ Q) → (P ∨ (Q ∧ A)))) replace proposition variable C by P ∨ A in 132
134 (D → ((P ∨ A) → ((P ∨ Q) → (P ∨ (Q ∧ A))))) → ((((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → D) → (((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → ((P ∨ A) → ((P ∨ Q) → (P ∨ (Q ∧ A)))))) replace proposition variable C by (P ∨ A) → ((P ∨ Q) → (P ∨ (Q ∧ A))) in 127
135 ((¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A)))) → ((P ∨ A) → ((P ∨ Q) → (P ∨ (Q ∧ A))))) → ((((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A))))) → (((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → ((P ∨ A) → ((P ∨ Q) → (P ∨ (Q ∧ A)))))) replace proposition variable D by ¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A))) in 134
136 (((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → (¬(P ∨ A) ∨ ((P ∨ Q) → (P ∨ (Q ∧ A))))) → (((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → ((P ∨ A) → ((P ∨ Q) → (P ∨ (Q ∧ A))))) modus ponens with 133, 135
137 ((P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A)))) → ((P ∨ A) → ((P ∨ Q) → (P ∨ (Q ∧ A)))) modus ponens with 131, 136
138 (P ∨ A) → ((P ∨ Q) → (P ∨ (Q ∧ A))) modus ponens with 83, 137
139 (D → ((P ∨ Q) → (P ∨ (Q ∧ A)))) → ((P ∨ Q) → (D → (P ∨ (Q ∧ A)))) replace proposition variable C by P ∨ Q in 25
140 ((P ∨ A) → ((P ∨ Q) → (P ∨ (Q ∧ A)))) → ((P ∨ Q) → ((P ∨ A) → (P ∨ (Q ∧ A)))) replace proposition variable D by P ∨ A in 139
141 (P ∨ Q) → ((P ∨ A) → (P ∨ (Q ∧ A))) modus ponens with 138, 140
142 (P → (Q → A)) → ((P ∧ Q) → A) add proposition hilb29
143 (P → (Q → B)) → ((P ∧ Q) → B) replace proposition variable A by B in 142
144 (P → (C → B)) → ((P ∧ C) → B) replace proposition variable Q by C in 143
145 (D → (C → B)) → ((D ∧ C) → B) replace proposition variable P by D in 144
146 (D → (C → (P ∨ (Q ∧ A)))) → ((D ∧ C) → (P ∨ (Q ∧ A))) replace proposition variable B by P ∨ (Q ∧ A) in 145
147 (D → ((P ∨ A) → (P ∨ (Q ∧ A)))) → ((D ∧ (P ∨ A)) → (P ∨ (Q ∧ A))) replace proposition variable C by P ∨ A in 146
148 ((P ∨ Q) → ((P ∨ A) → (P ∨ (Q ∧ A)))) → (((P ∨ Q) ∧ (P ∨ A)) → (P ∨ (Q ∧ A))) replace proposition variable D by P ∨ Q in 147
149 ((P ∨ Q) ∧ (P ∨ A)) → (P ∨ (Q ∧ A)) modus ponens with 141, 148
qed

A form for the abbreviation rule form for disjunction (first direction):

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

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

A form for the abbreviation rule form for disjunction (second direction):

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

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