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  2252  ax13ALT  2425  r19.30  3099  intss2  5058  vtoclr  5682  funopg  6521  feldmfvelcdm  7025  abnex  7696  xpider  8718  undifixp  8864  onsdominel  9045  fodomr  9047  fodomfir  9218  wemaplem2  9439  rankuni2b  9752  infxpenlem  9910  dfac8b  9928  ac10ct  9931  alephordi  9971  infdif  10105  cfflb  10156  alephval2  10469  tskxpss  10669  tskcard  10678  ingru  10712  grur1  10717  grothac  10727  suplem1pr  10949  mulgt0sr  11002  ixxssixx  13265  difelfzle  13547  swrdnd0  14571  climrlim2  15460  qshash  15740  gcdcllem3  16418  vdwlem13  16911  ocvsscon  21618  opsrtoslem2  21997  txcnp  23541  t0kq  23739  filconn  23804  filuni  23806  alexsubALTlem3  23970  rectbntr0  24754  iscau4  25212  cfilres  25229  lmcau  25246  bcthlem2  25258  onvf1odlem2  35155  subfacp1lem6  35236  cvmsdisj  35321  meran1  36462  bj-bi3ant  36640  bj-cbv3ta  36837  bj-2upleq  37063  bj-ismooredr2  37161  bj-snmoore  37164  bj-isclm  37342  relowlssretop  37414  poimirlem30  37696  poimirlem31  37697  caushft  37807  partimeq  38913  ax13fromc9  39011  harinf  43132  ntrk0kbimka  44137  onfrALTlem3  44642  onfrALTlem2  44644  e222  44734  e111  44772  e333  44830  bitr3VD  44946  disjinfi  45294  prpair  47606  onsetrec  49814  aacllem  49907