for questions or link request: module admin

# Further Theorems of Propositional Calculus

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

## Description

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

## References

This document uses the results of the following documents:

## Content

First distributive law (first direction):

1. Proposition
((P
Ú (Q Ù A)) ® ((P Ú Q) Ù (P Ú A)))     (hilb36)

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

First distributive law (second direction):

2. Proposition
(((P
Ú Q) Ù (P Ú A)) ® (P Ú (Q Ù A)))     (hilb37)

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

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

3. Proposition
((P
Ú Q) ® Ø(ØP Ù ØQ))     (hilb38)

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

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

4. Proposition
(
Ø(ØP Ù ØQ) ® (P Ú Q))     (hilb39)

Proof:
 1 (ØØP ® P) add proposition hilb6 2 (ØØA ® A) replace proposition variable P by A in 1 3 (ØØ(P Ú Q) ® (P Ú Q)) replace proposition variable A by (P Ú Q) in 2 4 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1 5 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2 6 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 7 ((P Ú A) ® (A Ú P)) replace proposition variable Q by A in 6 8 ((B Ú A) ® (A Ú B)) replace proposition variable P by B in 7 9 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1 10 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 9 11 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 10 12 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 11 13 ((B Ú (P Ú Q)) ® ((P Ú Q) Ú B)) replace proposition variable A by (P Ú Q) in 8 14 ((P ® A) ® (ØP Ú A)) replace proposition variable Q by A in 4 15 ((B ® A) ® (ØB Ú A)) replace proposition variable P by B in 14 16 ((B ® (P Ú Q)) ® (ØB Ú (P Ú Q))) replace proposition variable A by (P Ú Q) in 15 17 ((ØP Ú A) ® (P ® A)) replace proposition variable Q by A in 5 18 ((ØB Ú A) ® (B ® A)) replace proposition variable P by B in 17 19 ((ØB Ú (P Ú Q)) ® (B ® (P Ú Q))) replace proposition variable A by (P Ú Q) in 18 20 (ØØQ ® Q) replace proposition variable P by Q in 1 21 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 22 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 21 23 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 22 24 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 23 25 ((D ® C) ® ((Q Ú D) ® (Q Ú C))) replace proposition variable B by Q in 24 26 ((D ® P) ® ((Q Ú D) ® (Q Ú P))) replace proposition variable C by P in 25 27 ((ØØP ® P) ® ((Q Ú ØØP) ® (Q Ú P))) replace proposition variable D by ØØP in 26 28 ((Q Ú ØØP) ® (Q Ú P)) modus ponens with 1, 27 29 ((B Ú P) ® (P Ú B)) replace proposition variable A by P in 8 30 ((Q Ú P) ® (P Ú Q)) replace proposition variable B by Q in 29 31 ((D ® C) ® (((Q Ú ØØP) ® D) ® ((Q Ú ØØP) ® C))) replace proposition variable B by (Q Ú ØØP) in 12 32 ((D ® (P Ú Q)) ® (((Q Ú ØØP) ® D) ® ((Q Ú ØØP) ® (P Ú Q)))) replace proposition variable C by (P Ú Q) in 31 33 (((Q Ú P) ® (P Ú Q)) ® (((Q Ú ØØP) ® (Q Ú P)) ® ((Q Ú ØØP) ® (P Ú Q)))) replace proposition variable D by (Q Ú P) in 32 34 (((Q Ú ØØP) ® (Q Ú P)) ® ((Q Ú ØØP) ® (P Ú Q))) modus ponens with 30, 33 35 ((Q Ú ØØP) ® (P Ú Q)) modus ponens with 28, 34 36 ((B Ú Q) ® (Q Ú B)) replace proposition variable A by Q in 8 37 ((ØØP Ú Q) ® (Q Ú ØØP)) replace proposition variable B by ØØP in 36 38 ((D ® C) ® (((ØØP Ú Q) ® D) ® ((ØØP Ú Q) ® C))) replace proposition variable B by (ØØP Ú Q) in 12 39 ((D ® (P Ú Q)) ® (((ØØP Ú Q) ® D) ® ((ØØP Ú Q) ® (P Ú Q)))) replace proposition variable C by (P Ú Q) in 38 40 (((Q Ú ØØP) ® (P Ú Q)) ® (((ØØP Ú Q) ® (Q Ú ØØP)) ® ((ØØP Ú Q) ® (P Ú Q)))) replace proposition variable D by (Q Ú ØØP) in 39 41 (((ØØP Ú Q) ® (Q Ú ØØP)) ® ((ØØP Ú Q) ® (P Ú Q))) modus ponens with 35, 40 42 ((ØØP Ú Q) ® (P Ú Q)) modus ponens with 37, 41 43 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7 44 ((P ® A) ® (ØA ® ØP)) replace proposition variable Q by A in 43 45 ((B ® A) ® (ØA ® ØB)) replace proposition variable P by B in 44 46 ((B ® (P Ú Q)) ® (Ø(P Ú Q) ® ØB)) replace proposition variable A by (P Ú Q) in 45 47 (((ØØP Ú Q) ® (P Ú Q)) ® (Ø(P Ú Q) ® Ø(ØØP Ú Q))) replace proposition variable B by (ØØP Ú Q) in 46 48 (Ø(P Ú Q) ® Ø(ØØP Ú Q)) modus ponens with 42, 47 49 ((B ® Ø(ØØP Ú Q)) ® (ØØ(ØØP Ú Q) ® ØB)) replace proposition variable A by Ø(ØØP Ú Q) in 45 50 ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(ØØP Ú Q) ® ØØ(P Ú Q))) replace proposition variable B by Ø(P Ú Q) in 49 51 (ØØ(ØØP Ú Q) ® ØØ(P Ú Q)) modus ponens with 48, 50 52 ((B ® ØØ(P Ú Q)) ® (ØØØ(P Ú Q) ® ØB)) replace proposition variable A by ØØ(P Ú Q) in 45 53 ((ØØ(ØØP Ú Q) ® ØØ(P Ú Q)) ® (ØØØ(P Ú Q) ® ØØØ(ØØP Ú Q))) replace proposition variable B by ØØ(ØØP Ú Q) in 52 54 (ØØØ(P Ú Q) ® ØØØ(ØØP Ú Q)) modus ponens with 51, 53 55 ((D ® C) ® (((P Ú Q) Ú D) ® ((P Ú Q) Ú C))) replace proposition variable B by (P Ú Q) in 24 56 ((D ® ØØØ(ØØP Ú Q)) ® (((P Ú Q) Ú D) ® ((P Ú Q) Ú ØØØ(ØØP Ú Q)))) replace proposition variable C by ØØØ(ØØP Ú Q) in 55 57 ((ØØØ(P Ú Q) ® ØØØ(ØØP Ú Q)) ® (((P Ú Q) Ú ØØØ(P Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú Q)))) replace proposition variable D by ØØØ(P Ú Q) in 56 58 (((P Ú Q) Ú ØØØ(P Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú Q))) modus ponens with 54, 57 59 ((B Ú ØØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú Q) Ú B)) replace proposition variable A by ØØØ(ØØP Ú Q) in 8 60 (((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))) replace proposition variable B by (P Ú Q) in 59 61 ((D ® C) ® ((((P Ú Q) Ú ØØØ(P Ú Q)) ® D) ® (((P Ú Q) Ú ØØØ(P Ú Q)) ® C))) replace proposition variable B by ((P Ú Q) Ú ØØØ(P Ú Q)) in 12 62 ((D ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))) ® ((((P Ú Q) Ú ØØØ(P Ú Q)) ® D) ® (((P Ú Q) Ú ØØØ(P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))))) replace proposition variable C by (ØØØ(ØØP Ú Q) Ú (P Ú Q)) in 61 63 ((((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))) ® ((((P Ú Q) Ú ØØØ(P Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú Q))) ® (((P Ú Q) Ú ØØØ(P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))))) replace proposition variable D by ((P Ú Q) Ú ØØØ(ØØP Ú Q)) in 62 64 ((((P Ú Q) Ú ØØØ(P Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú Q))) ® (((P Ú Q) Ú ØØØ(P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q)))) modus ponens with 60, 63 65 (((P Ú Q) Ú ØØØ(P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))) modus ponens with 58, 64 66 ((ØØØ(P Ú Q) Ú (P Ú Q)) ® ((P Ú Q) Ú ØØØ(P Ú Q))) replace proposition variable B by ØØØ(P Ú Q) in 13 67 ((D ® C) ® (((ØØØ(P Ú Q) Ú (P Ú Q)) ® D) ® ((ØØØ(P Ú Q) Ú (P Ú Q)) ® C))) replace proposition variable B by (ØØØ(P Ú Q) Ú (P Ú Q)) in 12 68 ((D ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))) ® (((ØØØ(P Ú Q) Ú (P Ú Q)) ® D) ® ((ØØØ(P Ú Q) Ú (P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))))) replace proposition variable C by (ØØØ(ØØP Ú Q) Ú (P Ú Q)) in 67 69 ((((P Ú Q) Ú ØØØ(P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))) ® (((ØØØ(P Ú Q) Ú (P Ú Q)) ® ((P Ú Q) Ú ØØØ(P Ú Q))) ® ((ØØØ(P Ú Q) Ú (P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))))) replace proposition variable D by ((P Ú Q) Ú ØØØ(P Ú Q)) in 68 70 (((ØØØ(P Ú Q) Ú (P Ú Q)) ® ((P Ú Q) Ú ØØØ(P Ú Q))) ® ((ØØØ(P Ú Q) Ú (P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q)))) modus ponens with 65, 69 71 ((ØØØ(P Ú Q) Ú (P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))) modus ponens with 66, 70 72 ((ØØ(P Ú Q) ® (P Ú Q)) ® (ØØØ(P Ú Q) Ú (P Ú Q))) replace proposition variable B by ØØ(P Ú Q) in 16 73 ((D ® C) ® (((ØØ(P Ú Q) ® (P Ú Q)) ® D) ® ((ØØ(P Ú Q) ® (P Ú Q)) ® C))) replace proposition variable B by (ØØ(P Ú Q) ® (P Ú Q)) in 12 74 ((D ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))) ® (((ØØ(P Ú Q) ® (P Ú Q)) ® D) ® ((ØØ(P Ú Q) ® (P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))))) replace proposition variable C by (ØØØ(ØØP Ú Q) Ú (P Ú Q)) in 73 75 (((ØØØ(P Ú Q) Ú (P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))) ® (((ØØ(P Ú Q) ® (P Ú Q)) ® (ØØØ(P Ú Q) Ú (P Ú Q))) ® ((ØØ(P Ú Q) ® (P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))))) replace proposition variable D by (ØØØ(P Ú Q) Ú (P Ú Q)) in 74 76 (((ØØ(P Ú Q) ® (P Ú Q)) ® (ØØØ(P Ú Q) Ú (P Ú Q))) ® ((ØØ(P Ú Q) ® (P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q)))) modus ponens with 71, 75 77 ((ØØ(P Ú Q) ® (P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))) modus ponens with 72, 76 78 ((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® (ØØ(ØØP Ú Q) ® (P Ú Q))) replace proposition variable B by ØØ(ØØP Ú Q) in 19 79 ((D ® (ØØ(ØØP Ú Q) ® (P Ú Q))) ® (((ØØ(P Ú Q) ® (P Ú Q)) ® D) ® ((ØØ(P Ú Q) ® (P Ú Q)) ® (ØØ(ØØP Ú Q) ® (P Ú Q))))) replace proposition variable C by (ØØ(ØØP Ú Q) ® (P Ú Q)) in 73 80 (((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® (ØØ(ØØP Ú Q) ® (P Ú Q))) ® (((ØØ(P Ú Q) ® (P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))) ® ((ØØ(P Ú Q) ® (P Ú Q)) ® (ØØ(ØØP Ú Q) ® (P Ú Q))))) replace proposition variable D by (ØØØ(ØØP Ú Q) Ú (P Ú Q)) in 79 81 (((ØØ(P Ú Q) ® (P Ú Q)) ® (ØØØ(ØØP Ú Q) Ú (P Ú Q))) ® ((ØØ(P Ú Q) ® (P Ú Q)) ® (ØØ(ØØP Ú Q) ® (P Ú Q)))) modus ponens with 78, 80 82 ((ØØ(P Ú Q) ® (P Ú Q)) ® (ØØ(ØØP Ú Q) ® (P Ú Q))) modus ponens with 77, 81 83 (ØØ(ØØP Ú Q) ® (P Ú Q)) modus ponens with 3, 82 84 ((D ® C) ® ((ØØP Ú D) ® (ØØP Ú C))) replace proposition variable B by ØØP in 24 85 ((D ® Q) ® ((ØØP Ú D) ® (ØØP Ú Q))) replace proposition variable C by Q in 84 86 ((ØØQ ® Q) ® ((ØØP Ú ØØQ) ® (ØØP Ú Q))) replace proposition variable D by ØØQ in 85 87 ((ØØP Ú ØØQ) ® (ØØP Ú Q)) modus ponens with 20, 86 88 ((B ® (ØØP Ú Q)) ® (Ø(ØØP Ú Q) ® ØB)) replace proposition variable A by (ØØP Ú Q) in 45 89 (((ØØP Ú ØØQ) ® (ØØP Ú Q)) ® (Ø(ØØP Ú Q) ® Ø(ØØP Ú ØØQ))) replace proposition variable B by (ØØP Ú ØØQ) in 88 90 (Ø(ØØP Ú Q) ® Ø(ØØP Ú ØØQ)) modus ponens with 87, 89 91 ((B ® Ø(ØØP Ú ØØQ)) ® (ØØ(ØØP Ú ØØQ) ® ØB)) replace proposition variable A by Ø(ØØP Ú ØØQ) in 45 92 ((Ø(ØØP Ú Q) ® Ø(ØØP Ú ØØQ)) ® (ØØ(ØØP Ú ØØQ) ® ØØ(ØØP Ú Q))) replace proposition variable B by Ø(ØØP Ú Q) in 91 93 (ØØ(ØØP Ú ØØQ) ® ØØ(ØØP Ú Q)) modus ponens with 90, 92 94 ((B ® ØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú Q) ® ØB)) replace proposition variable A by ØØ(ØØP Ú Q) in 45 95 ((ØØ(ØØP Ú ØØQ) ® ØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú Q) ® ØØØ(ØØP Ú ØØQ))) replace proposition variable B by ØØ(ØØP Ú ØØQ) in 94 96 (ØØØ(ØØP Ú Q) ® ØØØ(ØØP Ú ØØQ)) modus ponens with 93, 95 97 ((D ® ØØØ(ØØP Ú ØØQ)) ® (((P Ú Q) Ú D) ® ((P Ú Q) Ú ØØØ(ØØP Ú ØØQ)))) replace proposition variable C by ØØØ(ØØP Ú ØØQ) in 55 98 ((ØØØ(ØØP Ú Q) ® ØØØ(ØØP Ú ØØQ)) ® (((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú ØØQ)))) replace proposition variable D by ØØØ(ØØP Ú Q) in 97 99 (((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú ØØQ))) modus ponens with 96, 98 100 ((B Ú ØØØ(ØØP Ú ØØQ)) ® (ØØØ(ØØP Ú ØØQ) Ú B)) replace proposition variable A by ØØØ(ØØP Ú ØØQ) in 8 101 (((P Ú Q) Ú ØØØ(ØØP Ú ØØQ)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))) replace proposition variable B by (P Ú Q) in 100 102 ((D ® C) ® ((((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® D) ® (((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® C))) replace proposition variable B by ((P Ú Q) Ú ØØØ(ØØP Ú Q)) in 12 103 ((D ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))) ® ((((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® D) ® (((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))))) replace proposition variable C by (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q)) in 102 104 ((((P Ú Q) Ú ØØØ(ØØP Ú ØØQ)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))) ® ((((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú ØØQ))) ® (((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))))) replace proposition variable D by ((P Ú Q) Ú ØØØ(ØØP Ú ØØQ)) in 103 105 ((((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú ØØQ))) ® (((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q)))) modus ponens with 101, 104 106 (((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))) modus ponens with 99, 105 107 ((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú Q))) replace proposition variable B by ØØØ(ØØP Ú Q) in 13 108 ((D ® C) ® (((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® D) ® ((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® C))) replace proposition variable B by (ØØØ(ØØP Ú Q) Ú (P Ú Q)) in 12 109 ((D ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))) ® (((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® D) ® ((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))))) replace proposition variable C by (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q)) in 108 110 ((((P Ú Q) Ú ØØØ(ØØP Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))) ® (((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú Q))) ® ((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® (ØØØ(ØØP Ú ØØQ) Ú (P Ú Q))))) replace proposition variable D by ((P Ú Q) Ú ØØØ(ØØP Ú Q)) in 109 111 (((ØØØ(ØØP Ú Q) Ú (P Ú Q)) ® ((P Ú Q) Ú ØØØ(ØØP Ú Q))) ® ((ØØØ(ØØ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:
 1 (((P Ú Q) Ù (P Ú A)) ® (P Ú (Q Ù A))) add proposition hilb37 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) Ù (P Ú A)) ® (P Ú (Q Ù A))) ® (Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A)))) replace proposition variable B by ((P Ú Q) Ù (P Ú A)) in 5 7 (Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú 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) Ù (P Ú A)) Ú D) ® (Ø((P Ú Q) Ù (P Ú A)) Ú C))) replace proposition variable B by Ø((P Ú Q) Ù (P Ú A)) in 14 30 ((D ® ØØ(P Ú ØØ(Q Ù A))) ® ((Ø((P Ú Q) Ù (P Ú A)) Ú D) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A))))) replace proposition variable C by ØØ(P Ú ØØ(Q Ù A)) in 29 31 ((ØØ(P Ú (Q Ù A)) ® ØØ(P Ú ØØ(Q Ù A))) ® ((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A))))) replace proposition variable D by ØØ(P Ú (Q Ù A)) in 30 32 ((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú 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) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) replace proposition variable C by Ø((P Ú Q) Ù (P Ú 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) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® D) ® ((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® C))) replace proposition variable B by (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) in 41 43 ((D ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® (((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® D) ® ((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))))) replace proposition variable C by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 42 44 (((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® (((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A)))) ® ((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))))) replace proposition variable D by (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A))) in 43 45 (((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú ØØ(Q Ù A)))) ® ((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))))) modus ponens with 37, 44 46 ((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) modus ponens with 32, 45 47 ((C Ú Ø((P Ú Q) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú C)) replace proposition variable B by Ø((P Ú Q) Ù (P Ú A)) in 35 48 ((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A)))) replace proposition variable C by ØØ(P Ú (Q Ù A)) in 47 49 ((D ® C) ® (((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® C))) replace proposition variable B by (ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 41 50 ((D ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® (((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))))) replace proposition variable C by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 49 51 (((Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® (((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A)))) ® ((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))))) replace proposition variable D by (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A))) in 50 52 (((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) Ú ØØ(P Ú (Q Ù A)))) ® ((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))))) modus ponens with 46, 51 53 ((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú 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) Ù (P Ú A))) ® (ØC Ú Ø((P Ú Q) Ù (P Ú A)))) replace proposition variable B by Ø((P Ú Q) Ù (P Ú A)) in 55 57 ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) replace proposition variable C by Ø(P Ú (Q Ù A)) in 56 58 ((D ® C) ® (((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® C))) replace proposition variable B by (Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) in 41 59 ((D ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))))) replace proposition variable C by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 58 60 (((ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))))) replace proposition variable D by (ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 59 61 (((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú (Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))))) modus ponens with 53, 60 62 ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú 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) Ù (P Ú A))) ® (C ® Ø((P Ú Q) Ù (P Ú A)))) replace proposition variable B by Ø((P Ú Q) Ù (P Ú A)) in 64 66 ((ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A)))) replace proposition variable C by Ø(P Ú ØØ(Q Ù A)) in 65 67 ((D ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A)))))) replace proposition variable C by (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) in 58 68 (((ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A)))))) replace proposition variable D by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 67 69 (((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))))) modus ponens with 66, 68 70 ((Ø(P Ú (Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A)))) modus ponens with 62, 69 71 (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú 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 ((P Ù Q) ® Ø(ØP Ú ØQ)) add proposition defand1 76 (Ø(ØP Ú ØQ) ® (P Ù Q)) add proposition defand2 77 ((B ® (P Ú Q)) ® (Ø(P Ú Q) ® ØB)) replace proposition variable A by (P Ú Q) in 4 78 ((ØØ(P Ú Q) ® (P Ú Q)) ® (Ø(P Ú Q) ® ØØØ(P Ú Q))) replace proposition variable B by ØØ(P Ú Q) in 77 79 (Ø(P Ú Q) ® ØØØ(P Ú Q)) modus ponens with 74, 78 80 ((D ® C) ® ((Ø(P Ú A) Ú D) ® (Ø(P Ú A) Ú C))) replace proposition variable B by Ø(P Ú A) in 14 81 ((D ® ØØØ(P Ú Q)) ® ((Ø(P Ú A) Ú D) ® (Ø(P Ú A) Ú ØØØ(P Ú Q)))) replace proposition variable C by ØØØ(P Ú Q) in 80 82 ((Ø(P Ú Q) ® ØØØ(P Ú Q)) ® ((Ø(P Ú A) Ú Ø(P Ú Q)) ® (Ø(P Ú A) Ú ØØØ(P Ú Q)))) replace proposition variable D by Ø(P Ú Q) in 81 83 ((Ø(P Ú A) Ú Ø(P Ú Q)) ® (Ø(P Ú A) Ú ØØØ(P Ú Q))) modus ponens with 79, 82 84 ((C Ú ØØØ(P Ú Q)) ® (ØØØ(P Ú Q) Ú C)) replace proposition variable B by ØØØ(P Ú Q) in 35 85 ((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) replace proposition variable C by Ø(P Ú A) in 84 86 ((D ® C) ® (((Ø(P Ú A) Ú Ø(P Ú Q)) ® D) ® ((Ø(P Ú A) Ú Ø(P Ú Q)) ® C))) replace proposition variable B by (Ø(P Ú A) Ú Ø(P Ú Q)) in 41 87 ((D ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((Ø(P Ú A) Ú Ø(P Ú Q)) ® D) ® ((Ø(P Ú A) Ú Ø(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))))) replace proposition variable C by (ØØØ(P Ú Q) Ú Ø(P Ú A)) in 86 88 (((Ø(P Ú A) Ú ØØØ(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((Ø(P Ú A) Ú Ø(P Ú Q)) ® (Ø(P Ú A) Ú ØØØ(P Ú Q))) ® ((Ø(P Ú A) Ú Ø(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))))) replace proposition variable D by (Ø(P Ú A) Ú ØØØ(P Ú Q)) in 87 89 (((Ø(P Ú A) Ú Ø(P Ú Q)) ® (Ø(P Ú A) Ú ØØØ(P Ú Q))) ® ((Ø(P Ú A) Ú Ø(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A)))) modus ponens with 85, 88 90 ((Ø(P Ú A) Ú Ø(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) modus ponens with 83, 89 91 ((C Ú Ø(P Ú A)) ® (Ø(P Ú A) Ú C)) replace proposition variable B by Ø(P Ú A) in 35 92 ((Ø(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú A) Ú Ø(P Ú Q))) replace proposition variable C by Ø(P Ú Q) in 91 93 ((D ® C) ® (((Ø(P Ú Q) Ú Ø(P Ú A)) ® D) ® ((Ø(P Ú Q) Ú Ø(P Ú A)) ® C))) replace proposition variable B by (Ø(P Ú Q) Ú Ø(P Ú A)) in 41 94 ((D ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((Ø(P Ú Q) Ú Ø(P Ú A)) ® D) ® ((Ø(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))))) replace proposition variable C by (ØØØ(P Ú Q) Ú Ø(P Ú A)) in 93 95 (((Ø(P Ú A) Ú Ø(P Ú Q)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((Ø(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú A) Ú Ø(P Ú Q))) ® ((Ø(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))))) replace proposition variable D by (Ø(P Ú A) Ú Ø(P Ú Q)) in 94 96 (((Ø(P Ú Q) Ú Ø(P Ú A)) ® (Ø(P Ú A) Ú Ø(P Ú Q))) ® ((Ø(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A)))) modus ponens with 90, 95 97 ((Ø(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) modus ponens with 92, 96 98 ((C ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® ØC)) replace proposition variable B by (ØØØ(P Ú Q) Ú Ø(P Ú A)) in 20 99 (((Ø(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A)))) replace proposition variable C by (Ø(P Ú Q) Ú Ø(P Ú A)) in 98 100 (Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))) modus ponens with 97, 99 101 ((P Ù B) ® Ø(ØP Ú ØB)) replace proposition variable Q by B in 75 102 ((C Ù B) ® Ø(ØC Ú ØB)) replace proposition variable P by C in 101 103 ((C Ù (P Ú A)) ® Ø(ØC Ú Ø(P Ú A))) replace proposition variable B by (P Ú A) in 102 104 ((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) replace proposition variable C by ØØ(P Ú Q) in 103 105 ((D ® C) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® C))) replace proposition variable B by (ØØ(P Ú Q) Ù (P Ú A)) in 41 106 ((D ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))))) replace proposition variable C by Ø(Ø(P Ú Q) Ú Ø(P Ú A)) in 105 107 ((Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))))) replace proposition variable D by Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) in 106 108 (((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A)))) modus ponens with 100, 107 109 ((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))) modus ponens with 104, 108 110 (Ø(ØP Ú ØB) ® (P Ù B)) replace proposition variable Q by B in 76 111 (Ø(ØC Ú ØB) ® (C Ù B)) replace proposition variable P by C in 110 112 (Ø(ØC Ú Ø(P Ú A)) ® (C Ù (P Ú A))) replace proposition variable B by (P Ú A) in 111 113 (Ø(Ø(P Ú Q) Ú Ø(P Ú A)) ® ((P Ú Q) Ù (P Ú A))) replace proposition variable C by (P Ú Q) in 112 114 ((D ® ((P Ú Q) Ù (P Ú A))) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® ((P Ú Q) Ù (P Ú A))))) replace proposition variable C by ((P Ú Q) Ù (P Ú A)) in 105 115 ((Ø(Ø(P Ú Q) Ú Ø(P Ú A)) ® ((P Ú Q) Ù (P Ú A))) ® (((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® ((P Ú Q) Ù (P Ú A))))) replace proposition variable D by Ø(Ø(P Ú Q) Ú Ø(P Ú A)) in 114 116 (((ØØ(P Ú Q) Ù (P Ú A)) ® Ø(Ø(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù (P Ú A)) ® ((P Ú Q) Ù (P Ú A)))) modus ponens with 113, 115 117 ((ØØ(P Ú Q) Ù (P Ú A)) ® ((P Ú Q) Ù (P Ú A))) modus ponens with 109, 116 118 ((C ® ((P Ú Q) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) ® ØC)) replace proposition variable B by ((P Ú Q) Ù (P Ú A)) in 20 119 (((ØØ(P Ú Q) Ù (P Ú A)) ® ((P Ú Q) Ù (P Ú A))) ® (Ø((P Ú Q) Ù (P Ú A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A)))) replace proposition variable C by (ØØ(P Ú Q) Ù (P Ú A)) in 118 120 (Ø((P Ú Q) Ù (P Ú A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) modus ponens with 117, 119 121 ((D ® C) ® ((ØØ(P Ú ØØ(Q Ù A)) Ú D) ® (ØØ(P Ú ØØ(Q Ù A)) Ú C))) replace proposition variable B by ØØ(P Ú ØØ(Q Ù A)) in 14 122 ((D ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® ((ØØ(P Ú ØØ(Q Ù A)) Ú D) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))))) replace proposition variable C by Ø(ØØ(P Ú Q) Ù (P Ú A)) in 121 123 ((Ø((P Ú Q) Ù (P Ú A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® ((ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))))) replace proposition variable D by Ø((P Ú Q) Ù (P Ú A)) in 122 124 ((ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) modus ponens with 120, 123 125 ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) replace proposition variable C by Ø(P Ú ØØ(Q Ù A)) in 56 126 ((D ® C) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® C))) replace proposition variable B by (Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) in 41 127 ((D ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))))) replace proposition variable C by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) in 126 128 (((ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))))) replace proposition variable D by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A))) in 127 129 (((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø((P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))))) modus ponens with 124, 128 130 ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) modus ponens with 125, 129 131 ((ØC Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (C ® Ø(ØØ(P Ú Q) Ù (P Ú A)))) replace proposition variable B by Ø(ØØ(P Ú Q) Ù (P Ú A)) in 64 132 ((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A)))) replace proposition variable C by Ø(P Ú ØØ(Q Ù A)) in 131 133 ((D ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A)))))) replace proposition variable C by (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) in 126 134 (((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A)))))) replace proposition variable D by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) in 133 135 (((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))))) modus ponens with 132, 134 136 ((Ø(P Ú ØØ(Q Ù A)) ® Ø((P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A)))) modus ponens with 130, 135 137 (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) modus ponens with 71, 136 138 (ØØB ® B) replace proposition variable P by B in 72 139 (ØØ(P Ú A) ® (P Ú A)) replace proposition variable B by (P Ú A) in 138 140 ((C ® (P Ú A)) ® (Ø(P Ú A) ® ØC)) replace proposition variable B by (P Ú A) in 20 141 ((ØØ(P Ú A) ® (P Ú A)) ® (Ø(P Ú A) ® ØØØ(P Ú A))) replace proposition variable C by ØØ(P Ú A) in 140 142 (Ø(P Ú A) ® ØØØ(P Ú A)) modus ponens with 139, 141 143 ((D ® C) ® ((ØØØ(P Ú Q) Ú D) ® (ØØØ(P Ú Q) Ú C))) replace proposition variable B by ØØØ(P Ú Q) in 14 144 ((D ® ØØØ(P Ú A)) ® ((ØØØ(P Ú Q) Ú D) ® (ØØØ(P Ú Q) Ú ØØØ(P Ú A)))) replace proposition variable C by ØØØ(P Ú A) in 143 145 ((Ø(P Ú A) ® ØØØ(P Ú A)) ® ((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú ØØØ(P Ú A)))) replace proposition variable D by Ø(P Ú A) in 144 146 ((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú ØØØ(P Ú A))) modus ponens with 142, 145 147 ((C ® (ØØØ(P Ú Q) Ú ØØØ(P Ú A))) ® (Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) ® ØC)) replace proposition variable B by (ØØØ(P Ú Q) Ú ØØØ(P Ú A)) in 20 148 (((ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (ØØØ(P Ú Q) Ú ØØØ(P Ú A))) ® (Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)))) replace proposition variable C by (ØØØ(P Ú Q) Ú Ø(P Ú A)) in 147 149 (Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) modus ponens with 146, 148 150 ((C Ù ØØ(P Ú A)) ® Ø(ØC Ú ØØØ(P Ú A))) replace proposition variable B by ØØ(P Ú A) in 102 151 ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A))) replace proposition variable C by ØØ(P Ú Q) in 150 152 ((D ® C) ® (((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® C))) replace proposition variable B by (ØØ(P Ú Q) Ù ØØ(P Ú A)) in 41 153 ((D ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))))) replace proposition variable C by Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) in 152 154 ((Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® (((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A))) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))))) replace proposition variable D by Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A)) in 153 155 (((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú ØØØ(P Ú A))) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)))) modus ponens with 149, 154 156 ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) modus ponens with 151, 155 157 (Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A))) replace proposition variable C by ØØ(P Ú Q) in 112 158 ((D ® (ØØ(P Ú Q) Ù (P Ú A))) ® (((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® D) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A))))) replace proposition variable C by (ØØ(P Ú Q) Ù (P Ú A)) in 152 159 ((Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A))) ® (((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A))))) replace proposition variable D by Ø(ØØØ(P Ú Q) Ú Ø(P Ú A)) in 158 160 (((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® Ø(ØØØ(P Ú Q) Ú Ø(P Ú A))) ® ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A)))) modus ponens with 157, 159 161 ((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A))) modus ponens with 156, 160 162 ((C ® (ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® ØC)) replace proposition variable B by (ØØ(P Ú Q) Ù (P Ú A)) in 20 163 (((ØØ(P Ú Q) Ù ØØ(P Ú A)) ® (ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) replace proposition variable C by (ØØ(P Ú Q) Ù ØØ(P Ú A)) in 162 164 (Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) modus ponens with 161, 163 165 ((D ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® ((ØØ(P Ú ØØ(Q Ù A)) Ú D) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))) replace proposition variable C by Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) in 121 166 ((Ø(ØØ(P Ú Q) Ù (P Ú A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® ((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))) replace proposition variable D by Ø(ØØ(P Ú Q) Ù (P Ú A)) in 165 167 ((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) modus ponens with 164, 166 168 ((C ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØC Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) replace proposition variable B by Ø(ØØ(P Ú Q) Ù (P Ú A)) in 55 169 ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) replace proposition variable C by Ø(P Ú ØØ(Q Ù A)) in 168 170 ((D ® C) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® C))) replace proposition variable B by (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) in 41 171 ((D ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))))) replace proposition variable C by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) in 170 172 (((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))))) replace proposition variable D by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A))) in 171 173 (((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù (P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))) modus ponens with 167, 172 174 ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) modus ponens with 169, 173 175 ((ØC Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® (C ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) replace proposition variable B by Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) in 64 176 ((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) replace proposition variable C by Ø(P Ú ØØ(Q Ù A)) in 175 177 ((D ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® D) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))))) replace proposition variable C by (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) in 170 178 (((ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® (((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))))) replace proposition variable D by (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) in 177 179 (((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (ØØ(P Ú ØØ(Q Ù A)) Ú Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) ® ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))))) modus ponens with 176, 178 180 ((Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù (P Ú A))) ® (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)))) modus ponens with 174, 179 181 (Ø(P Ú ØØ(Q Ù A)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) modus ponens with 137, 180 182 (Ø(P Ú ØØ(Q Ù B)) ® Ø(ØØ(P Ú Q) Ù ØØ(P Ú B))) replace proposition variable A by B in 181 183 (Ø(P Ú ØØ(C Ù B)) ® Ø(ØØ(P Ú C) Ù ØØ(P Ú B))) replace proposition variable Q by C in 182 184 (Ø(D Ú ØØ(C Ù B)) ® Ø(ØØ(D Ú C) Ù ØØ(D Ú B))) replace proposition variable P by D in 183 185 (Ø(D Ú ØØ(C Ù ØA)) ® Ø(ØØ(D Ú C) Ù ØØ(D Ú ØA))) replace proposition variable B by ØA in 184 186 (Ø(D Ú ØØ(ØQ Ù ØA)) ® Ø(ØØ(D Ú ØQ) Ù ØØ(D Ú ØA))) replace proposition variable C by ØQ in 185 187 (Ø(ØP Ú ØØ(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) replace proposition variable D by ØP in 186 188 ((P Ù Ø(ØQ Ù ØA)) ® Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) reverse abbreviation and in 187 at occurence 1 189 ((P Ú Q) ® Ø(ØP Ù ØQ)) add proposition hilb38 190 ((P Ú B) ® Ø(ØP Ù ØB)) replace proposition variable Q by B in 189 191 ((C Ú B) ® Ø(ØC Ù ØB)) replace proposition variable P by C in 190 192 ((C Ú A) ® Ø(ØC Ù ØA)) replace proposition variable B by A in 191 193 ((Q Ú A) ® Ø(ØQ Ù ØA)) replace proposition variable C by Q in 192 194 ((C ® Ø(ØQ Ù ØA)) ® (ØØ(ØQ Ù ØA) ® ØC)) replace proposition variable B by Ø(ØQ Ù ØA) in 20 195 (((Q Ú A) ® Ø(ØQ Ù ØA)) ® (ØØ(ØQ Ù ØA) ® Ø(Q Ú A))) replace proposition variable C by (Q Ú A) in 194 196 (ØØ(ØQ Ù ØA) ® Ø(Q Ú A)) modus ponens with 193, 195 197 ((D ® C) ® ((ØP Ú D) ® (ØP Ú C))) replace proposition variable B by ØP in 14 198 ((D ® Ø(Q Ú A)) ® ((ØP Ú D) ® (ØP Ú Ø(Q Ú A)))) replace proposition variable C by Ø(Q Ú A) in 197 199 ((ØØ(ØQ Ù ØA) ® Ø(Q Ú A)) ® ((ØP Ú ØØ(ØQ Ù ØA)) ® (ØP Ú Ø(Q Ú A)))) replace proposition variable D by ØØ(ØQ Ù ØA) in 198 200 ((ØP Ú ØØ(ØQ Ù ØA)) ® (ØP Ú Ø(Q Ú A))) modus ponens with 196, 199 201 ((C ® (ØP Ú Ø(Q Ú A))) ® (Ø(ØP Ú Ø(Q Ú A)) ® ØC)) replace proposition variable B by (ØP Ú Ø(Q Ú A)) in 20 202 (((ØP Ú ØØ(ØQ Ù ØA)) ® (ØP Ú Ø(Q Ú A))) ® (Ø(ØP Ú Ø(Q Ú A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA)))) replace proposition variable C by (ØP Ú ØØ(ØQ Ù ØA)) in 201 203 (Ø(ØP Ú Ø(Q Ú A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA))) modus ponens with 200, 202 204 ((C Ù (Q Ú A)) ® Ø(ØC Ú Ø(Q Ú A))) replace proposition variable B by (Q Ú A) in 102 205 ((P Ù (Q Ú A)) ® Ø(ØP Ú Ø(Q Ú A))) replace proposition variable C by P in 204 206 ((D ® C) ® (((P Ù (Q Ú A)) ® D) ® ((P Ù (Q Ú A)) ® C))) replace proposition variable B by (P Ù (Q Ú A)) in 41 207 ((D ® Ø(ØP Ú ØØ(ØQ Ù ØA))) ® (((P Ù (Q Ú A)) ® D) ® ((P Ù (Q Ú A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA))))) replace proposition variable C by Ø(ØP Ú ØØ(ØQ Ù ØA)) in 206 208 ((Ø(Ø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 207 209 (((P Ù (Q Ú A)) ® Ø(ØP Ú Ø(Q Ú A))) ® ((P Ù (Q Ú A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA)))) modus ponens with 203, 208 210 ((P Ù (Q Ú A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA))) modus ponens with 205, 209 211 (Ø(ØC Ú ØØ(ØQ Ù ØA)) ® (C Ù Ø(ØQ Ù ØA))) replace proposition variable B by Ø(ØQ Ù ØA) in 111 212 (Ø(ØP Ú ØØ(ØQ Ù ØA)) ® (P Ù Ø(ØQ Ù ØA))) replace proposition variable C by P in 211 213 ((D ® (P Ù Ø(ØQ Ù ØA))) ® (((P Ù (Q Ú A)) ® D) ® ((P Ù (Q Ú A)) ® (P Ù Ø(ØQ Ù ØA))))) replace proposition variable C by (P Ù Ø(ØQ Ù ØA)) in 206 214 ((Ø(Ø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 213 215 (((P Ù (Q Ú A)) ® Ø(ØP Ú ØØ(ØQ Ù ØA))) ® ((P Ù (Q Ú A)) ® (P Ù Ø(ØQ Ù ØA)))) modus ponens with 212, 214 216 ((P Ù (Q Ú A)) ® (P Ù Ø(ØQ Ù ØA))) modus ponens with 210, 215 217 ((C ® (P Ù Ø(ØQ Ù ØA))) ® (Ø(P Ù Ø(ØQ Ù ØA)) ® ØC)) replace proposition variable B by (P Ù Ø(ØQ Ù ØA)) in 20 218 (((P Ù (Q Ú A)) ® (P Ù Ø(ØQ Ù ØA))) ® (Ø(P Ù Ø(ØQ Ù ØA)) ® Ø(P Ù (Q Ú A)))) replace proposition variable C by (P Ù (Q Ú A)) in 217 219 (Ø(P Ù Ø(ØQ Ù ØA)) ® Ø(P Ù (Q Ú A))) modus ponens with 216, 218 220 ((D ® C) ® ((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú D) ® (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú C))) replace proposition variable B by Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) in 14 221 ((D ® Ø(P Ù (Q Ú A))) ® ((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú D) ® (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù (Q Ú A))))) replace proposition variable C by Ø(P Ù (Q Ú A)) in 220 222 ((Ø(P Ù Ø(ØQ Ù ØA)) ® Ø(P Ù (Q Ú A))) ® ((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù (Q Ú A))))) replace proposition variable D by Ø(P Ù Ø(ØQ Ù ØA)) in 221 223 ((Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Ú Ø(P Ù Ø(ØQ Ù ØA))) ® (Ø(