# Further Theorems of Propositional Calculus

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

## Description

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

## References

This document uses the results of the following documents:

## Content

First distributive law (first direction):

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

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

First distributive law (second direction):

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

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

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

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

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

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

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

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

By duality we get the second distributive law (first direction):

5. Proposition
(P ∧ (Q ∨ A)) → ((P ∧ Q) ∨ (P ∧ A))     (hilb40)

Proof: