Metamath Proof Explorer

Theorem tarski-bernays-ax2

Description: Derivation of ax-2 from the Tarski-Bernays axiom set { ax-1 , imim1 , peirce }. Note that no inference rule other than ax-mp is used in this proof. This proof establishes a circle of equivalence: From { impsingle }, { ax-1 , imim1 , peirce } was proved. From { ax-1 , imim1 , peirce }, { ax-1 , ax-2 and peirce } was proved. From { ax-1 , ax-2 and peirce }, { impsingle } was proved. Therefore, the theorems that can be proved by selecting any one of these three distinct axiom sets must be equivalent. Prover9 and mmj2 were used to help constuct this proof. (Contributed by Larry Lesyna and Jeffrey P. Machado, 1-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion tarski-bernays-ax2 
|- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )

Proof

Step Hyp Ref Expression
1 peirce 
 |-  ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) )
2 ax-1 
 |-  ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
3 1 2 ax-mp 
 |-  ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
4 imim1 
 |-  ( ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
5 3 4 ax-mp 
 |-  ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
6 peirce 
 |-  ( ( ( ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
7 imim1 
 |-  ( ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
8 imim1 
 |-  ( ( ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ( ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) ) )
9 7 8 ax-mp 
 |-  ( ( ( ( ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
10 6 9 ax-mp 
 |-  ( ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
11 5 10 ax-mp 
 |-  ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
12 imim1 
 |-  ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
13 imim1 
 |-  ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
14 12 13 ax-mp 
 |-  ( ( ( ( ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
15 11 14 ax-mp 
 |-  ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
16 imim1 
 |-  ( ( ( ( ph -> ch ) -> ch ) -> ( ( ps -> ch ) -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) ) )
17 imim1 
 |-  ( ( ( ( ( ph -> ch ) -> ch ) -> ( ( ps -> ch ) -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ch ) -> ch ) -> ( ( ps -> ch ) -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
18 16 17 ax-mp 
 |-  ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ph -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ch ) -> ch ) -> ( ( ps -> ch ) -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
19 15 18 ax-mp 
 |-  ( ( ( ( ph -> ch ) -> ch ) -> ( ( ps -> ch ) -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
20 imim1 
 |-  ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ph -> ch ) -> ch ) -> ( ( ps -> ch ) -> ch ) ) )
21 imim1 
 |-  ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ph -> ch ) -> ch ) -> ( ( ps -> ch ) -> ch ) ) ) -> ( ( ( ( ( ph -> ch ) -> ch ) -> ( ( ps -> ch ) -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
22 20 21 ax-mp 
 |-  ( ( ( ( ( ph -> ch ) -> ch ) -> ( ( ps -> ch ) -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
23 19 22 ax-mp 
 |-  ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
24 peirce 
 |-  ( ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
25 imim1 
 |-  ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
26 imim1 
 |-  ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
27 25 26 ax-mp 
 |-  ( ( ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
28 24 27 ax-mp 
 |-  ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
29 imim1 
 |-  ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
30 imim1 
 |-  ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
31 29 30 ax-mp 
 |-  ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
32 28 31 ax-mp 
 |-  ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
33 ax-1 
 |-  ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) ) )
34 imim1 
 |-  ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
35 33 34 ax-mp 
 |-  ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
36 32 35 ax-mp 
 |-  ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
37 imim1 
 |-  ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
38 imim1 
 |-  ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) ) )
39 37 38 ax-mp 
 |-  ( ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
40 imim1 
 |-  ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
41 imim1 
 |-  ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) ) ) )
42 40 41 ax-mp 
 |-  ( ( ( ( ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) ) )
43 39 42 ax-mp 
 |-  ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
44 36 43 ax-mp 
 |-  ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
45 23 44 ax-mp 
 |-  ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
46 imim1 
 |-  ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) )
47 imim1 
 |-  ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
48 46 47 ax-mp 
 |-  ( ( ( ( ( ps -> ch ) -> ch ) -> ( ph -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
49 45 48 ax-mp 
 |-  ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
50 peirce 
 |-  ( ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
51 imim1 
 |-  ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
52 imim1 
 |-  ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
53 51 52 ax-mp 
 |-  ( ( ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
54 50 53 ax-mp 
 |-  ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
55 imim1 
 |-  ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
56 imim1 
 |-  ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
57 55 56 ax-mp 
 |-  ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
58 54 57 ax-mp 
 |-  ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
59 ax-1 
 |-  ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) )
60 imim1 
 |-  ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
61 59 60 ax-mp 
 |-  ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
62 58 61 ax-mp 
 |-  ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
63 imim1 
 |-  ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) )
64 imim1 
 |-  ( ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) )
65 63 64 ax-mp 
 |-  ( ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) )
66 imim1 
 |-  ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) )
67 imim1 
 |-  ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) ) )
68 66 67 ax-mp 
 |-  ( ( ( ( ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) )
69 65 68 ax-mp 
 |-  ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) )
70 62 69 ax-mp 
 |-  ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) )
71 49 70 ax-mp 
 |-  ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )
72 imim1 
 |-  ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )
73 imim1 
 |-  ( ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) -> ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) )
74 72 73 ax-mp 
 |-  ( ( ( ( ps -> ch ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) )
75 71 74 ax-mp 
 |-  ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )
76 peirce 
 |-  ( ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
77 imim1 
 |-  ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
78 imim1 
 |-  ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
79 77 78 ax-mp 
 |-  ( ( ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
80 76 79 ax-mp 
 |-  ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
81 imim1 
 |-  ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
82 imim1 
 |-  ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
83 81 82 ax-mp 
 |-  ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
84 80 83 ax-mp 
 |-  ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
85 ax-1 
 |-  ( ( ph -> ( ps -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) )
86 imim1 
 |-  ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) ) -> ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) ) )
87 85 86 ax-mp 
 |-  ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) )
88 84 87 ax-mp 
 |-  ( ( ph -> ( ps -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
89 imim1 
 |-  ( ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) )
90 imim1 
 |-  ( ( ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) ) )
91 89 90 ax-mp 
 |-  ( ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) )
92 imim1 
 |-  ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) )
93 imim1 
 |-  ( ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) ) ) )
94 92 93 ax-mp 
 |-  ( ( ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) ) )
95 91 94 ax-mp 
 |-  ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) ) )
96 88 95 ax-mp 
 |-  ( ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) )
97 75 96 ax-mp 
 |-  ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )