Metamath Proof Explorer

Theorem adh-minimp-ax2c

Description: Derivation of a commuted form of ax-2 from adh-minimp and ax-mp . Polish prefix notation: CCpqCCpCqrCpr . (Contributed by BJ, 4-Apr-2021) (Revised by ADH, 10-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 adh-minimp-jarr-ax2c-lem3 
 |-  ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ph )
2 adh-minimp-jarr-imim1-ax2c-lem1 
 |-  ( ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ph ) -> ( ( ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) ) )
3 1 2 ax-mp 
 |-  ( ( ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) )
4 adh-minimp-sylsimp 
 |-  ( ( ( ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) ) )
5 3 4 ax-mp 
 |-  ( ( ph -> ( ps -> ch ) ) -> ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) )
6 adh-minimp-jarr-imim1-ax2c-lem1 
 |-  ( ( ( ph -> ( ps -> ch ) ) -> ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) ) -> ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) )
7 5 6 ax-mp 
 |-  ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )
8 adh-minimp-sylsimp 
 |-  ( ( ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) -> ( ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) )
9 7 8 ax-mp 
 |-  ( ( ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )
10 adh-minimp-jarr-imim1-ax2c-lem1 
 |-  ( ( ph -> ps ) -> ( ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) )
11 adh-minimp-imim1 
 |-  ( ( ( ph -> ps ) -> ( ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) )
12 10 11 ax-mp 
 |-  ( ( ( ( ( ( ( th -> ta ) -> ( ( ( et -> th ) -> ( ta -> ze ) ) -> ( th -> ze ) ) ) -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) )
13 9 12 ax-mp 
 |-  ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )