# First theorems of Propositional Calculus

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

## Description

This module includes first proofs of propositional 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 we prove a simple implication, that follows directly from the fourth axiom:

1. Proposition
((P
® Q) ® ((A ® P) ® (A ® Q)))     (hilb1)

Proof:
 1 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 2 ((P ® Q) ® ((ØA Ú P) ® (ØA Ú Q))) replace proposition variable A by ØA in 1 3 ((P ® Q) ® ((A ® P) ® (ØA Ú Q))) reverse abbreviation impl in 2 at occurence 1 4 ((P ® Q) ® ((A ® P) ® (A ® Q))) reverse abbreviation impl in 3 at occurence 1 qed

This proposition is the form for the Hypothetical Syllogism.

The self implication could be derived:

2. Proposition
(P
® P)     (hilb2)

Proof:
 1 (P ® (P Ú Q)) add axiom axiom2 2 (P ® (P Ú P)) replace proposition variable Q by P in 1 3 ((P Ú P) ® P) add axiom axiom1 4 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1 5 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 4 6 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 5 7 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 6 8 ((D ® C) ® ((P ® D) ® (P ® C))) replace proposition variable B by P in 7 9 ((D ® P) ® ((P ® D) ® (P ® P))) replace proposition variable C by P in 8 10 (((P Ú P) ® P) ® ((P ® (P Ú P)) ® (P ® P))) replace proposition variable D by (P Ú P) in 9 11 ((P ® (P Ú P)) ® (P ® P)) modus ponens with 3, 10 12 (P ® P) modus ponens with 2, 11 qed

One form of the classical `tertium non datur'

3. Proposition
(
ØP Ú P)     (hilb3)

Proof:
 1 (P ® P) add proposition hilb2 2 (ØP Ú P) use abbreviation impl in 1 at occurence 1 qed

The standard form of the excluded middle:

4. Proposition
(P
Ú ØP)     (hilb4)

Proof:
 1 (ØP Ú P) add proposition hilb3 2 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 3 ((P Ú A) ® (A Ú P)) replace proposition variable Q by A in 2 4 ((B Ú A) ® (A Ú B)) replace proposition variable P by B in 3 5 ((B Ú P) ® (P Ú B)) replace proposition variable A by P in 4 6 ((ØP Ú P) ® (P Ú ØP)) replace proposition variable B by ØP in 5 7 (P Ú ØP) modus ponens with 1, 6 qed

Double negation is implicated:

5. Proposition
(P
® ØØP)     (hilb5)

Proof:
 1 (P Ú ØP) add proposition hilb4 2 (ØP Ú ØØP) replace proposition variable P by ØP in 1 3 (P ® ØØP) reverse abbreviation impl in 2 at occurence 1 qed

The reverse is also true:

6. Proposition
(
ØØP ® P)     (hilb6)

Proof:
 1 (P ® ØØP) add proposition hilb5 2 (ØP ® ØØØP) replace proposition variable P by ØP in 1 3 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 4 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 3 5 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 4 6 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 5 7 ((D ® C) ® ((P Ú D) ® (P Ú C))) replace proposition variable B by P in 6 8 ((D ® ØØØP) ® ((P Ú D) ® (P Ú ØØØP))) replace proposition variable C by ØØØP in 7 9 ((ØP ® ØØØP) ® ((P Ú ØP) ® (P Ú ØØØP))) replace proposition variable D by ØP in 8 10 ((P Ú ØP) ® (P Ú ØØØP)) modus ponens with 2, 9 11 (P Ú ØP) add proposition hilb4 12 (P Ú ØØØP) modus ponens with 11, 10 13 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 14 ((P Ú A) ® (A Ú P)) replace proposition variable Q by A in 13 15 ((B Ú A) ® (A Ú B)) replace proposition variable P by B in 14 16 ((B Ú ØØØP) ® (ØØØP Ú B)) replace proposition variable A by ØØØP in 15 17 ((P Ú ØØØP) ® (ØØØP Ú P)) replace proposition variable B by P in 16 18 (ØØØP Ú P) modus ponens with 12, 17 19 (ØØP ® P) reverse abbreviation impl in 18 at occurence 1 qed

The correct reverse of an implication:

7. Proposition
((P
® Q) ® (ØQ ® ØP))     (hilb7)

Proof:
 1 (P ® ØØP) add proposition hilb5 2 (Q ® ØØQ) replace proposition variable P by Q in 1 3 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 4 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 3 5 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 4 6 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 5 7 ((D ® C) ® ((ØP Ú D) ® (ØP Ú C))) replace proposition variable B by ØP in 6 8 ((D ® ØØQ) ® ((ØP Ú D) ® (ØP Ú ØØQ))) replace proposition variable C by ØØQ in 7 9 ((Q ® ØØQ) ® ((ØP Ú Q) ® (ØP Ú ØØQ))) replace proposition variable D by Q in 8 10 ((ØP Ú Q) ® (ØP Ú ØØQ)) modus ponens with 2, 9 11 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 12 ((P Ú A) ® (A Ú P)) replace proposition variable Q by A in 11 13 ((B Ú A) ® (A Ú B)) replace proposition variable P by B in 12 14 ((B Ú ØØQ) ® (ØØQ Ú B)) replace proposition variable A by ØØQ in 13 15 ((ØP Ú ØØQ) ® (ØØQ Ú ØP)) replace proposition variable B by ØP in 14 16 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1 17 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 16 18 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 17 19 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 18 20 ((D ® C) ® (((ØP Ú Q) ® D) ® ((ØP Ú Q) ® C))) replace proposition variable B by (ØP Ú Q) in 19 21 ((D ® (ØØQ Ú ØP)) ® (((ØP Ú Q) ® D) ® ((ØP Ú Q) ® (ØØQ Ú ØP)))) replace proposition variable C by (ØØQ Ú ØP) in 20 22 (((ØP Ú ØØQ) ® (ØØQ Ú ØP)) ® (((ØP Ú Q) ® (ØP Ú ØØQ)) ® ((ØP Ú Q) ® (ØØQ Ú ØP)))) replace proposition variable D by (ØP Ú ØØQ) in 21 23 (((ØP Ú Q) ® (ØP Ú ØØQ)) ® ((ØP Ú Q) ® (ØØQ Ú ØP))) modus ponens with 15, 22 24 ((ØP Ú Q) ® (ØØQ Ú ØP)) modus ponens with 10, 23 25 ((P ® Q) ® (ØØQ Ú ØP)) reverse abbreviation impl in 24 at occurence 1 26 ((P ® Q) ® (ØQ ® ØP)) reverse abbreviation impl in 25 at occurence 1 qed

Definition of an Implication 1. part:

8. Proposition
((P
® Q) ® (ØP Ú Q))     (defimpl1)

Proof:
 1 (P ® P) add proposition hilb2 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)) use abbreviation impl in 3 at occurence 3 qed

Definition of an Implication 2. part:

9. Proposition
((
ØP Ú Q) ® (P ® Q))     (defimpl2)

Proof:
 1 (P ® P) add proposition hilb2 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)) use abbreviation impl in 3 at occurence 2 qed

Definition of a Conjunction 1. part:

10. Proposition
((P
Ù Q) ® Ø(ØP Ú ØQ))     (defand1)

Proof:
 1 (P ® P) add proposition hilb2 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)) use abbreviation and in 3 at occurence 2 qed

Definition of a Conjunction 2. part:

11. Proposition
(
Ø(ØP Ú ØQ) ® (P Ù Q))     (defand2)

Proof:
 1 (P ® P) add proposition hilb2 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)) use abbreviation and in 3 at occurence 1 qed

Definition of an Equivalence 1. part:

12. Proposition
((P
« Q) ® ((P ® Q) Ù (Q ® P)))     (defequi1)

Proof:
 1 (P ® P) add proposition hilb2 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) Ù (Q ® P))) use abbreviation equi in 3 at occurence 2 qed

Definition of an Equivalence 2. part:

13. Proposition
(((P
® Q) Ù (Q ® P)) ® (P « Q))     (defequi2)

Proof:
 1 (P ® P) add proposition hilb2 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) Ù (Q ® P)) ® (P « Q)) use abbreviation equi in 3 at occurence 1 qed

A simular formulation for the second axiom:

14. Proposition
(P
® (Q Ú P))     (hilb8)

Proof:
 1 (P ® (P Ú Q)) add axiom axiom2 2 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 3 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1 4 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 3 5 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 4 6 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 5 7 ((D ® C) ® ((P ® D) ® (P ® C))) replace proposition variable B by P in 6 8 ((D ® (Q Ú P)) ® ((P ® D) ® (P ® (Q Ú P)))) replace proposition variable C by (Q Ú P) in 7 9 (((P Ú Q) ® (Q Ú P)) ® ((P ® (P Ú Q)) ® (P ® (Q Ú P)))) replace proposition variable D by (P Ú Q) in 8 10 ((P ® (P Ú Q)) ® (P ® (Q Ú P))) modus ponens with 2, 9 11 (P ® (Q Ú P)) modus ponens with 1, 10 qed

A technical lemma (equal to the third axiom):

15. Proposition
((P
Ú Q) ® (Q Ú P))     (hilb9)

Proof:
 1 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 qed

And another technical lemma (simular to the third axiom):

16. Proposition
((Q
Ú P) ® (P Ú Q))     (hilb10)

Proof:
 1 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 2 ((P Ú A) ® (A Ú P)) replace proposition variable Q by A in 1 3 ((B Ú A) ® (A Ú B)) replace proposition variable P by B in 2 4 ((B Ú P) ® (P Ú B)) replace proposition variable A by P in 3 5 ((Q Ú P) ® (P Ú Q)) replace proposition variable B by Q in 4 qed

A technical lemma (equal to the first axiom):

17. Proposition
((P
Ú P) ® P)     (hilb11)

Proof:
 1 ((P Ú P) ® P) add axiom axiom1 qed

A simple propositon that follows directly from the second axiom:

18. Proposition
(P
® (P Ú P))     (hilb12)

Proof:
 1 (P ® (P Ú Q)) add axiom axiom2 2 (P ® (P Ú P)) replace proposition variable Q by P in 1 qed

This is a pre form for the associative law:

19. Proposition
((P
Ú (Q Ú A)) ® (Q Ú (P Ú A)))     (hilb13)

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

The associative law for the disjunction (first direction):

20. Proposition
((P
Ú (Q Ú A)) ® ((P Ú Q) Ú A))     (hilb14)

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

The associative law for the disjunction (second direction):

21. Proposition
(((P
Ú Q) Ú A) ® (P Ú (Q Ú A)))     (hilb15)

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

Another consequence from hilb13 is the exchange of preconditions:

22. Proposition
((P
® (Q ® A)) ® (Q ® (P ® A)))     (hilb16)

Proof:
 1 ((P Ú (Q Ú A)) ® (Q Ú (P Ú A))) add proposition hilb13 2 ((P Ú (Q Ú B)) ® (Q Ú (P Ú B))) replace proposition variable A by B in 1 3 ((P Ú (C Ú B)) ® (C Ú (P Ú B))) replace proposition variable Q by C in 2 4 ((D Ú (C Ú B)) ® (C Ú (D Ú B))) replace proposition variable P by D in 3 5 ((D Ú (C Ú A)) ® (C Ú (D Ú A))) replace proposition variable B by A in 4 6 ((D Ú (ØQ Ú A)) ® (ØQ Ú (D Ú A))) replace proposition variable C by ØQ in 5 7 ((ØP Ú (ØQ Ú A)) ® (ØQ Ú (ØP Ú A))) replace proposition variable D by ØP in 6 8 ((P ® (ØQ Ú A)) ® (ØQ Ú (ØP Ú A))) reverse abbreviation impl in 7 at occurence 1 9 ((P ® (Q ® A)) ® (ØQ Ú (ØP Ú A))) reverse abbreviation impl in 8 at occurence 1 10 ((P ® (Q ® A)) ® (Q ® (ØP Ú A))) reverse abbreviation impl in 9 at occurence 1 11 ((P ® (Q ® A)) ® (Q ® (P ® A))) reverse abbreviation impl in 10 at occurence 1 qed

An analogus form for hyperref [hilb16]hilb16:

23. Proposition
((Q
® (P ® A)) ® (P ® (Q ® A)))     (hilb17)

Proof:
 1 ((P ® (Q ® A)) ® (Q ® (P ® A))) add proposition hilb16 2 ((P ® (Q ® B)) ® (Q ® (P ® B))) replace proposition variable A by B in 1 3 ((P ® (C ® B)) ® (C ® (P ® B))) replace proposition variable Q by C in 2 4 ((D ® (C ® B)) ® (C ® (D ® B))) replace proposition variable P by D in 3 5 ((D ® (C ® A)) ® (C ® (D ® A))) replace proposition variable B by A in 4 6 ((D ® (P ® A)) ® (P ® (D ® A))) replace proposition variable C by P in 5 7 ((Q ® (P ® A)) ® (P ® (Q ® A))) replace proposition variable D by Q in 6 qed

## Cross References

This document is used by the following documents: