Metamath Proof Explorer

Theorem imim12

Description: Closed form of imim12i and of 3syl . (Contributed by BJ, 16-Jul-2019)

Ref Expression
Assertion imim12 
|- ( ( ph -> ps ) -> ( ( ch -> th ) -> ( ( ps -> ch ) -> ( ph -> th ) ) ) )

Proof

Step Hyp Ref Expression
1 imim2 
 |-  ( ( ch -> th ) -> ( ( ps -> ch ) -> ( ps -> th ) ) )
2 imim1 
 |-  ( ( ph -> ps ) -> ( ( ps -> th ) -> ( ph -> th ) ) )
3 1 2 syl9r 
 |-  ( ( ph -> ps ) -> ( ( ch -> th ) -> ( ( ps -> ch ) -> ( ph -> th ) ) ) )