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  4573  vtoclr  4803  funopg  5391  xpider  6853  rerecapb  9134  ixxssixx  10254  difelfzle  10490  txcnp  15262  uspgr2wlkeqi  16488  bj-inf2vnlem1  16866