Metamath Proof Explorer

Theorem minimp-ax2c

Description: Derivation of a commuted form of ax-2 from ax-mp and minimp . (Contributed by BJ, 4-Apr-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion minimp-ax2c 
|- ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )

Proof

Step Hyp Ref Expression
1 minimp 
 |-  ( ph -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) )
2 minimp 
 |-  ( ( ph -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) -> ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) )
3 1 2 ax-mp 
 |-  ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) )
4 minimp 
 |-  ( ( ph -> ( ps -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) ) ) )
5 minimp 
 |-  ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) ) ) )
6 minimp 
 |-  ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) )
7 minimp 
 |-  ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) ) ) )
8 minimp 
 |-  ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) )
9 minimp 
 |-  ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) ) ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) -> ( ( ( ph -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) ) )
10 7 8 9 mp2 
 |-  ( ( ( ph -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) )
11 minimp 
 |-  ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) ) ) ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) -> ( ( ( ( ph -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ph ) ) ) )
12 5 11 ax-mp 
 |-  ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) -> ( ( ( ( ph -> ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ph ) ) )
13 6 10 12 mp2 
 |-  ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ph )
14 minimp 
 |-  ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) ) ) ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ph ) -> ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) ) ) )
15 5 13 14 mp2 
 |-  ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) )
16 minimp-syllsimp 
 |-  ( ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) ) )
17 15 16 ax-mp 
 |-  ( ( ph -> ( ps -> ch ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) )
18 minimp 
 |-  ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) ) ) ) -> ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) ) -> ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) )
19 4 17 18 mp2 
 |-  ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )
20 minimp-syllsimp 
 |-  ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) )
21 19 20 ax-mp 
 |-  ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )
22 minimp 
 |-  ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) ) )
23 minimp 
 |-  ( ( ph -> ps ) -> ( ( ( ph -> ps ) -> ( ph -> ps ) ) -> ( ( ( ( ph -> ps ) -> ( ph -> ps ) ) -> ( ( ph -> ps ) -> ( ph -> ps ) ) ) -> ( ( ph -> ps ) -> ( ph -> ps ) ) ) ) )
24 minimp 
 |-  ( ( ( ph -> ps ) -> ( ( ( ph -> ps ) -> ( ph -> ps ) ) -> ( ( ( ( ph -> ps ) -> ( ph -> ps ) ) -> ( ( ph -> ps ) -> ( ph -> ps ) ) ) -> ( ( ph -> ps ) -> ( ph -> ps ) ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ps ) -> ( ph -> ps ) ) -> ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) )
25 23 24 ax-mp 
 |-  ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ps ) -> ( ph -> ps ) ) -> ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) )
26 minimp 
 |-  ( ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) ) ) -> ( ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ph -> ps ) -> ( ph -> ps ) ) -> ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ph -> ps ) -> ( ph -> ps ) ) -> ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) ) ) )
27 22 25 26 mp2 
 |-  ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ph -> ps ) -> ( ph -> ps ) ) -> ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) )
28 minimp-syllsimp 
 |-  ( ( ( ( ( ph -> ps ) -> ( ph -> ps ) ) -> ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) )
29 minimp-syllsimp 
 |-  ( ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ph -> ps ) -> ( ph -> ps ) ) -> ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) ) -> ( ( ( ( ( ( ph -> ps ) -> ( ph -> ps ) ) -> ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) ) ) )
30 27 28 29 mp2 
 |-  ( ( ( ph -> ps ) -> ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ph -> ph ) -> ( ( ( ph -> ph ) -> ( ph -> ph ) ) -> ( ph -> ph ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) )
31 3 21 30 mp2 
 |-  ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )