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  3105  intss2  5051  vtoclr  5685  funopg  6524  feldmfvelcdm  7030  abnex  7702  xpider  8726  undifixp  8873  onsdominel  9055  fodomr  9057  fodomfir  9229  wemaplem2  9453  rankuni2b  9766  infxpenlem  9924  dfac8b  9942  ac10ct  9945  alephordi  9985  infdif  10119  cfflb  10170  alephval2  10484  tskxpss  10684  tskcard  10693  ingru  10727  grur1  10732  grothac  10742  suplem1pr  10964  mulgt0sr  11017  ixxssixx  13276  difelfzle  13558  swrdnd0  14582  climrlim2  15471  qshash  15751  gcdcllem3  16429  vdwlem13  16922  ocvsscon  21632  opsrtoslem2  22012  txcnp  23563  t0kq  23761  filconn  23826  filuni  23828  alexsubALTlem3  23992  rectbntr0  24776  iscau4  25224  cfilres  25241  lmcau  25258  bcthlem2  25270  onvf1odlem2  35292  subfacp1lem6  35373  cvmsdisj  35458  meran1  36599  bj-bi3ant  36852  bj-cbv3ta  37091  bj-2upleq  37317  bj-ismooredr2  37420  bj-snmoore  37423  bj-isclm  37603  relowlssretop  37675  poimirlem30  37962  poimirlem31  37963  caushft  38073  partimeq  39224  ax13fromc9  39343  harinf  43465  ntrk0kbimka  44469  onfrALTlem3  44974  onfrALTlem2  44976  e222  45066  e111  45104  e333  45162  bitr3VD  45278  disjinfi  45625  prpair  47935  onsetrec  50141  aacllem  50234