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  2246  ax13ALT  2427  r19.30  3117  intss2  5112  vtoclr  5751  funopg  6601  feldmfvelcdm  7105  abnex  7775  xpider  8826  undifixp  8972  onsdominel  9164  fodomr  9166  fodomfir  9365  wemaplem2  9584  rankuni2b  9890  infxpenlem  10050  dfac8b  10068  ac10ct  10071  alephordi  10111  infdif  10245  cfflb  10296  alephval2  10609  tskxpss  10809  tskcard  10818  ingru  10852  grur1  10857  grothac  10867  suplem1pr  11089  mulgt0sr  11142  ixxssixx  13397  difelfzle  13677  swrdnd0  14691  climrlim2  15579  qshash  15859  gcdcllem3  16534  vdwlem13  17026  ocvsscon  21710  opsrtoslem2  22097  txcnp  23643  t0kq  23841  filconn  23906  filuni  23908  alexsubALTlem3  24072  rectbntr0  24867  iscau4  25326  cfilres  25343  lmcau  25360  bcthlem2  25372  subfacp1lem6  35169  cvmsdisj  35254  meran1  36393  bj-bi3ant  36571  bj-cbv3ta  36768  bj-2upleq  36994  bj-ismooredr2  37092  bj-snmoore  37095  bj-isclm  37273  relowlssretop  37345  poimirlem30  37636  poimirlem31  37637  caushft  37747  partimeq  38790  ax13fromc9  38887  harinf  43022  ntrk0kbimka  44028  onfrALTlem3  44541  onfrALTlem2  44543  e222  44633  e111  44671  e333  44730  bitr3VD  44846  disjinfi  45134  prpair  47425  onsetrec  48938  aacllem  49031