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  2250  ax13ALT  2423  r19.30  3096  intss2  5060  vtoclr  5686  funopg  6520  feldmfvelcdm  7024  abnex  7697  xpider  8722  undifixp  8868  onsdominel  9050  fodomr  9052  fodomfir  9237  wemaplem2  9458  rankuni2b  9768  infxpenlem  9926  dfac8b  9944  ac10ct  9947  alephordi  9987  infdif  10121  cfflb  10172  alephval2  10485  tskxpss  10685  tskcard  10694  ingru  10728  grur1  10733  grothac  10743  suplem1pr  10965  mulgt0sr  11018  ixxssixx  13280  difelfzle  13562  swrdnd0  14582  climrlim2  15472  qshash  15752  gcdcllem3  16430  vdwlem13  16923  ocvsscon  21600  opsrtoslem2  21979  txcnp  23523  t0kq  23721  filconn  23786  filuni  23788  alexsubALTlem3  23952  rectbntr0  24737  iscau4  25195  cfilres  25212  lmcau  25229  bcthlem2  25241  onvf1odlem2  35076  subfacp1lem6  35157  cvmsdisj  35242  meran1  36384  bj-bi3ant  36562  bj-cbv3ta  36759  bj-2upleq  36985  bj-ismooredr2  37083  bj-snmoore  37086  bj-isclm  37264  relowlssretop  37336  poimirlem30  37629  poimirlem31  37630  caushft  37740  partimeq  38786  ax13fromc9  38884  harinf  43007  ntrk0kbimka  44012  onfrALTlem3  44518  onfrALTlem2  44520  e222  44610  e111  44648  e333  44706  bitr3VD  44822  disjinfi  45170  prpair  47486  onsetrec  49681  aacllem  49774