Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 585. (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  axc16gOLD  2336  ax13ALT  2473  vtoclr  5362  funopg  6133  abnex  7193  xpider  8051  undifixp  8179  onsdominel  8346  fodomr  8348  wemaplem2  8689  rankuni2b  8961  infxpenlem  9117  dfac8b  9135  ac10ct  9138  alephordi  9178  infdif  9314  cfflb  9364  alephval2  9677  tskxpss  9877  tskcard  9886  ingru  9920  grur1  9925  grothac  9935  suplem1pr  10157  mulgt0sr  10209  ixxssixx  12405  difelfzle  12674  climrlim2  14499  qshash  14779  gcdcllem3  15440  vdwlem13  15912  opsrtoslem2  19691  ocvsscon  20227  txcnp  21635  t0kq  21833  filconn  21898  filuni  21900  alexsubALTlem3  22064  rectbntr0  22846  iscau4  23287  cfilres  23304  lmcau  23321  bcthlem2  23332  clwlksfoclwwlkOLD  27235  subfacp1lem6  31488  cvmsdisj  31573  meran1  32725  bj-bi3ant  32887  bj-cbv3ta  33023  bj-2upleq  33308  bj-intss  33362  bj-snmoore  33377  relowlssretop  33525  poimirlem30  33750  poimirlem31  33751  caushft  33866  ax13fromc9  34683  harinf  38100  ntrk0kbimka  38835  onfrALTlem3  39255  onfrALTlem2  39257  e222  39357  e111  39395  e333  39455  bitr3VD  39576  onsetrec  43020  aacllem  43116