Theorem syl2imc 39

Description: A commuted version of syl2im 38. Implication-only version of syl2anr 290. (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 38	. 2 |- ( ph -> ( ch -> ta ) )
5	4	com12 30	1 |- ( ch -> ( ph -> ta ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  cnptopco  15323