Theorem syl2imc 41

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

Hypotheses

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

Assertion

Ref	Expression
syl2imc	|- ( ch -> ( ph -> ta ) )

Proof of Theorem syl2imc

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

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  triun  4766  undifixp  7944  rankpwi  8686  2cshwcshw  13571  incexclem  14568  sumeven  15110  cygth  19920  cnpco  21071  txkgen  21455  ontgval  32430  bj-dvelimdv1  32835  eel12131  38938  2ffzoeq  41338  iccpartgt  41363  bgoldbtbndlem3  41695