Metamath Proof Explorer

Theorem adh-minimp-imim1

Description: Derivation of imim1 ("left antimonotonicity of implication", theorem *2.06 of WhiteheadRussell p. 100) from adh-minimp and ax-mp . Polish prefix notation: CCpqCCqrCpr . (Contributed by ADH, 10-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 adh-minimp-sylsimp 
 |-  ( ( ( ( th -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )
2 adh-minimp-jarr-imim1-ax2c-lem1 
 |-  ( ( ph -> ps ) -> ( ( ( th -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) )
3 adh-minimp-jarr-imim1-ax2c-lem1 
 |-  ( ( ( ph -> ps ) -> ( ( ( th -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( rh -> ( ph -> ps ) ) -> ( ( ( ( th -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) )
4 2 3 ax-mp 
 |-  ( ( ( rh -> ( ph -> ps ) ) -> ( ( ( ( th -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) )
5 adh-minimp-sylsimp 
 |-  ( ( ( ( rh -> ( ph -> ps ) ) -> ( ( ( ( th -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( th -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) )
6 4 5 ax-mp 
 |-  ( ( ( ( ( th -> ph ) -> ( ps -> ch ) ) -> ( ph -> ch ) ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) -> ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) )
7 1 6 ax-mp 
 |-  ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )