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: