Metamath Proof Explorer

Theorem adh-minimp-jarr-lem2

Description: Second lemma for the derivation of jarr , and indirectly ax-1 , a commuted form of ax-2 , and ax-2 proper, from adh-minimp and ax-mp . Polish prefix notation: CCCpqCCCrsCCCtrCsuCruvCqv . (Contributed by ADH, 10-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion adh-minimp-jarr-lem2 
|- ( ( ( ph -> ps ) -> ( ( ( ch -> th ) -> ( ( ( ta -> ch ) -> ( th -> et ) ) -> ( ch -> et ) ) ) -> ze ) ) -> ( ps -> ze ) )

Proof

Step Hyp Ref Expression
1 adh-minimp 
 |-  ( ps -> ( ( ch -> th ) -> ( ( ( ta -> ch ) -> ( th -> et ) ) -> ( ch -> et ) ) ) )
2 adh-minimp-jarr-imim1-ax2c-lem1 
 |-  ( ( ps -> ( ( ch -> th ) -> ( ( ( ta -> ch ) -> ( th -> et ) ) -> ( ch -> et ) ) ) ) -> ( ( ( ph -> ps ) -> ( ( ( ch -> th ) -> ( ( ( ta -> ch ) -> ( th -> et ) ) -> ( ch -> et ) ) ) -> ze ) ) -> ( ps -> ze ) ) )
3 1 2 ax-mp 
 |-  ( ( ( ph -> ps ) -> ( ( ( ch -> th ) -> ( ( ( ta -> ch ) -> ( th -> et ) ) -> ( ch -> et ) ) ) -> ze ) ) -> ( ps -> ze ) )