for questions or link request: module admin

First theorems of Propositional Calculus

name: prophilbert1, module version: 1.00.00, rule version: 1.00.00, orignal: 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)

Uses the following modules:

Is used by the following modules:


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 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

This module is used by the following modules: