Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 595. (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  2240  ax13ALT  2423  r19.30  3119  intss2  5111  vtoclr  5739  funopg  6582  abnex  7748  xpider  8788  undifixp  8934  onsdominel  9132  fodomr  9134  wemaplem2  9548  rankuni2b  9854  infxpenlem  10014  dfac8b  10032  ac10ct  10035  alephordi  10075  infdif  10210  cfflb  10260  alephval2  10573  tskxpss  10773  tskcard  10782  ingru  10816  grur1  10821  grothac  10831  suplem1pr  11053  mulgt0sr  11106  ixxssixx  13345  difelfzle  13621  swrdnd0  14614  climrlim2  15498  qshash  15780  gcdcllem3  16449  vdwlem13  16933  ocvsscon  21538  opsrtoslem2  21928  txcnp  23444  t0kq  23642  filconn  23707  filuni  23709  alexsubALTlem3  23873  rectbntr0  24668  iscau4  25127  cfilres  25144  lmcau  25161  bcthlem2  25173  subfacp1lem6  34640  cvmsdisj  34725  meran1  35760  bj-bi3ant  35931  bj-cbv3ta  36128  bj-2upleq  36357  bj-ismooredr2  36455  bj-snmoore  36458  bj-isclm  36636  relowlssretop  36708  poimirlem30  36982  poimirlem31  36983  caushft  37093  partimeq  38143  ax13fromc9  38240  harinf  42236  ntrk0kbimka  43253  onfrALTlem3  43768  onfrALTlem2  43770  e222  43860  e111  43898  e333  43957  bitr3VD  44073  disjinfi  44350  prpair  46628  onsetrec  47915  aacllem  48010