for questions or link request: module admin

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: