Basic Rule of inference "From any wff of the form "Cab", and any other wff of the form "a", we may infer "b"."

Axioms:

Group 1:

1 CpCqp  Conditional-Simplification abbreviatied C-s
2 CCpCqrCCpqCpr Conditional-Self-Distribution  abbreviated C-d.

Group 2:

3 CCpKqNqNp  Negation-in  abbreviated Ni
4 CCNpKqNqp  Negation-out abbreviated No

Group 3:

5 CKpqp Conjunction-out left abbreviated Kol
6 CKpqq Conjunction-out right abbreviated Kor
7 CpCqKpq  Conjunction-in abbreviated Ki

Group 4:

8   CpApq Alternation-in left abbreviated Ail
9   CpAqp Alternation-in right abbreviated Air
10 CCpqCCrqCAprq Alternation-out abbreviated Ao

Group 5:

11 CEpqCpq Equivlaence-out right abbreviated Eor
12 CEpqCqp Equivalence-out left abbreviated Eol
13 CCpqCCqpEpq Equivalence-in abbreviated Ei

Lemma 0: Epp. It can end up helpful to use this as a minor premise.

1 ! p hypothesis
2 Cpp 1-1 C-in
3 Epp 2, 2 E-in

Lemma 1: {Epq, p} => q. Nickname: E-detach right.

1 Epq assumption
2 p assumption
3 Cpq 1 E-out left
4 q 3, 2 C-out

Lemma 2: {Epq, q} => p. Nickname: E-detach left.

1 Epq assumption
2 q assumption
3 Cqp 1 E-out right
4 p 2, 3 C-out

Lemma 3: |- EEpqEqp. Nickname: E-commutation.

1 !-1 Epq hypothesis
2 !-1 Cqp 1 E-out right
3 !-1 Cpq 1 E-out left
4 !-1 Eqp 2, 3 E-in
5 CEpqEqp 1-4 C-in
6 !-2 Eqp hypothesis
7 !-2 Cpq 6 E-out right
8 !-2 Cqp 6 E-out left
9 !-2 Epq 7, 8 E-in
10 CEqpEpq 6-9 C-in
11 EEpqEqp 6, 10 E-in

Lemma 4: |- ApNp. Nickname: law of the excluded middle.

1 ! NApNp hypothesis
2 @ Np hypothesis
3 @ ApNp 2 A-in
4 @ KApNpNApNp 3, 1 K-in
5 ! p 2-4 N-out
6 ! ApNp 5 A-in
7 ! KApNpNApNp 6, 1 K-in
8 ApNp 1-7 N-out

Lemma 5: {Cpq, Nq} => Np. Nickname: Modus Tollens.

1 Cpq assumption
2 Nq assumption
3 ! p hypothesis
4 ! q 3, 1 C-out
5 ! KqNq 2, 4 K-in
6 Np 3-5 N-out

Lemma 6: {Np, NEpq} => q. Nickname: Lemma 6.

1 Np assumption
2 NEpq assumption
3 !-1 Nq hypothesis
4 @-1 p hypothesis
5 #-1 Nq hypothesis
6 #-1 KpNp 4, 1 K-in
7 @-1 q 5-6 N-out
8 !-1 Cpq 4-7 C-in
9 @-2 q hypothesis
10 #-2 Np hypothesis
11 #-2 KqNq 9, 3 K-in
12 @-2 p 10-11 N-out
13 !-1 Cqp 9-12 C-in
14 !-1 Epq 8, 13 E-in
15 !-1 KEpqNEpq 14, 2 K-in
16 q 3-15 N-out

Lemma 7: {p, q} => Epq. Nickname: Lemma 7.

1 p assumption
2 q assumption
3 !-1 p hypothesis
4 !-1 q 2 Repitition
5 Cpq 3-4 C-in
6 !-2 q hypothesis
7 !-2 p 1 Repitition
8 Cqp 6-7 C-in
9 Epq 5, 8 E-in


Lemma 8: |- EEpEqrEEpqr. Nickname: E-association.

1 !-1 EpEqr hypothesis
2 @-1 Epq hypothesis
3 #-1 p hypothesis
4 #-1 Eqr 3, 1, E-detach right
5 #-1 q 3, 2, E-detach right
6 #-1 r 5, 4, E-detach right
7 @-1 Cpr 3-6 C-in
8 #-2 Np hypothesis
9 #-2 Cqp 2 E-out left
10 #-2 Nq 8, 9, Modus Tollens
11 #-2 CEqrp 1 E-out right
12 #-2 NEqr 8, 11, Modus Tollens
13 #-2 r 10, 12 Lemma 6
14 @-1 CNpr 8-13 C-in
15 @-1 ApNp law of the excluded middle
16 @-1 r 7, 14, 15 A-out
17 !-1 CEpqr 2-16 C-in
18 @-2 r hypothesis
19 #-3 p hypothesis
20 #-3 Eqr 19, 1, E-detach right
21 #-3 q 18, 20, E-detach left
22 @-2 Cpq 19-21 C-in
23 #-4 q hypothesis
24 #-4 CEqrp 1 E-out right
25 #-4 Eqr 23, 18, lemma 7
26 #-4 p 25, 24 C-out
27 @-2 Cqp 23-26 C-in
28 @-2 Epq 22, 27 E-in
29 !-1 CrEpq 18-28 C-in
30 !-1 EEpqr 17, 29 E-in
31 CEpEqrEEpqr 1-30 C-in
32 !-2 EEpqr hypothesis
33 @-3 p hypothesis
34 #-5 q hypothesis
35 #-5 Epq 33, 34 lemma 7
36 #-5 r 35, 32, E-detach right
37 @-3 Cqr 34-36 C-in
38 #-6 r hypothesis
39 #-6 Epq 38, 32, E-detach left
40 #-6 q 39, 33, E-detach right
41 @-3 Crq 38-40 C-in
42 @-3 Eqr 37, 41 E-in
43 !-2 CpEqr 33-42 C-in
44 @-4 Eqr hypothesis
45 #-7 r hypothesis
46 #-7 q 44, 45, E-detach left
47 #-7 Epq 45, 32, E-detach left
48 #-7 p 46, 47, E-detach right
49 @-4 Crp 45-48 C-in
50 #-8 Nr hypothesis
51 #-8 Cqr 44, E-out left
52 #-8 Nq 50, 51, Modus Tollens
53 #-8 CEpqr 32 E-out left
54 #-8 CEqpr 53, E-commutation
55 #-8 NEqp 50, 54, Modus Tollens
56 #-8 p 52, 55, lemma 6
57 @-4 CNrp 50-56 C-in
58 @-4 ArNr law of the excluded middle
59 @-4 p 49, 57, 58 A-out
60 !-2 CEqrp 44-59 C-in
61 !-2 EpEqr 43, 60 E-in
62 CEEpqrEpEqr 32-61 C-in
63 EEpEqrEEpqr 31, 62 E-in