Theorem syl2im 38

Description: Replace two antecedents. Implication-only version of syl2an 289. (Contributed by Wolf Lammen, 14-May-2013.)

Hypotheses

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

Assertion

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

Proof of Theorem syl2im

Step	Hyp	Ref	Expression
1		syl2im.1	. 2 |- ( ph -> ps )
2		syl2im.2	. . 3 |- ( ch -> th )
3		syl2im.3	. . 3 |- ( ps -> ( th -> ta ) )
4	2, 3	syl5 32	. 2 |- ( ps -> ( ch -> ta ) )
5	1, 4	syl 14	1 |- ( ph -> ( ch -> 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:  syl2imc  39  sylc  62  bi3ant  224  pm3.12dc  967  pm3.13dc  968  nfrimi  1574  abnex  4550  vtoclr  4780  funopg  5367  xpider  6818  rerecapb  9065  ixxssixx  10181  difelfzle  10414  txcnp  15065  uspgr2wlkeqi  16291  bj-inf2vnlem1  16669