Metamath Proof Explorer


Theorem syl2imc

Description: A commuted version of syl2im . Implication-only version of syl2anr . (Contributed by BJ, 20-Oct-2021)

Ref Expression
Hypotheses syl2im.1
|- ( ph -> ps )
syl2im.2
|- ( ch -> th )
syl2im.3
|- ( ps -> ( th -> ta ) )
Assertion syl2imc
|- ( ch -> ( ph -> ta ) )

Proof

Step Hyp Ref Expression
1 syl2im.1
 |-  ( ph -> ps )
2 syl2im.2
 |-  ( ch -> th )
3 syl2im.3
 |-  ( ps -> ( th -> ta ) )
4 1 2 3 syl2im
 |-  ( ph -> ( ch -> ta ) )
5 4 com12
 |-  ( ch -> ( ph -> ta ) )