Theorem syl2im 40

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

Hypotheses

Ref	Expression
syl2im.1	⊢ (𝜑 → 𝜓)
syl2im.2	⊢ (𝜒 → 𝜃)
syl2im.3	⊢ (𝜓 → (𝜃 → 𝜏))

Assertion

Ref	Expression
syl2im	⊢ (𝜑 → (𝜒 → 𝜏))

Proof of Theorem syl2im

Step	Hyp	Ref	Expression
1		syl2im.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl2im.2	. . 3 ⊢ (𝜒 → 𝜃)
3		syl2im.3	. . 3 ⊢ (𝜓 → (𝜃 → 𝜏))
4	2, 3	syl5 34	. 2 ⊢ (𝜓 → (𝜒 → 𝜏))
5	1, 4	syl 17	1 ⊢ (𝜑 → (𝜒 → 𝜏))

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  41  sylc  65  sbequ2  2241  ax13ALT  2424  r19.30  3120  intss2  5111  vtoclr  5739  funopg  6582  abnex  7743  xpider  8781  undifixp  8927  onsdominel  9125  fodomr  9127  wemaplem2  9541  rankuni2b  9847  infxpenlem  10007  dfac8b  10025  ac10ct  10028  alephordi  10068  infdif  10203  cfflb  10253  alephval2  10566  tskxpss  10766  tskcard  10775  ingru  10809  grur1  10814  grothac  10824  suplem1pr  11046  mulgt0sr  11099  ixxssixx  13337  difelfzle  13613  swrdnd0  14606  climrlim2  15490  qshash  15772  gcdcllem3  16441  vdwlem13  16925  ocvsscon  21227  opsrtoslem2  21616  txcnp  23123  t0kq  23321  filconn  23386  filuni  23388  alexsubALTlem3  23552  rectbntr0  24347  iscau4  24795  cfilres  24812  lmcau  24829  bcthlem2  24841  subfacp1lem6  34171  cvmsdisj  34256  meran1  35291  bj-bi3ant  35462  bj-cbv3ta  35659  bj-2upleq  35888  bj-ismooredr2  35986  bj-snmoore  35989  bj-isclm  36167  relowlssretop  36239  poimirlem30  36513  poimirlem31  36514  caushft  36624  partimeq  37674  ax13fromc9  37771  harinf  41763  ntrk0kbimka  42780  onfrALTlem3  43295  onfrALTlem2  43297  e222  43387  e111  43425  e333  43484  bitr3VD  43600  disjinfi  43881  prpair  46159  onsetrec  47743  aacllem  47838