Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 597. (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  2257  ax13ALT  2430  r19.30  3104  intss2  5064  vtoclr  5688  funopg  6527  feldmfvelcdm  7033  abnex  7704  xpider  8729  undifixp  8876  onsdominel  9058  fodomr  9060  fodomfir  9232  wemaplem2  9456  rankuni2b  9769  infxpenlem  9927  dfac8b  9945  ac10ct  9948  alephordi  9988  infdif  10122  cfflb  10173  alephval2  10487  tskxpss  10687  tskcard  10696  ingru  10730  grur1  10735  grothac  10745  suplem1pr  10967  mulgt0sr  11020  ixxssixx  13279  difelfzle  13561  swrdnd0  14585  climrlim2  15474  qshash  15754  gcdcllem3  16432  vdwlem13  16925  ocvsscon  21634  opsrtoslem2  22015  txcnp  23568  t0kq  23766  filconn  23831  filuni  23833  alexsubALTlem3  23997  rectbntr0  24781  iscau4  25239  cfilres  25256  lmcau  25273  bcthlem2  25285  onvf1odlem2  35279  subfacp1lem6  35360  cvmsdisj  35445  meran1  36586  bj-bi3ant  36764  bj-cbv3ta  36962  bj-2upleq  37188  bj-ismooredr2  37286  bj-snmoore  37289  bj-isclm  37467  relowlssretop  37539  poimirlem30  37822  poimirlem31  37823  caushft  37933  partimeq  39084  ax13fromc9  39203  harinf  43312  ntrk0kbimka  44316  onfrALTlem3  44821  onfrALTlem2  44823  e222  44913  e111  44951  e333  45009  bitr3VD  45125  disjinfi  45472  prpair  47783  onsetrec  49989  aacllem  50082