Theorem syl2im 41

Description: Replace two antecedents. Implication-only version of syl2an 608. (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 35	. 2 ⊢ (𝜓 → (𝜒 → 𝜏))
5	1, 4	syl 18	1 ⊢ (𝜑 → (𝜒 → 𝜏))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl2imc  42  sylc  66  sbequ2  2286  ax13ALT  2456  r19.30  3131  intss2  5072  vtoclr  5722  funopg  6571  feldmfvelcdm  7082  abnex  7759  xpider  8791  undifixp  8944  onsdominel  9127  fodomr  9129  fodomfir  9300  wemaplem2  9522  rankuni2b  9838  infxpenlem  10019  dfac8b  10037  alephordi  10080  infdif  10213  cfflb  10264  alephval2  10584  tskxpss  10784  tskcard  10793  ingru  10827  grur1  10832  grothac  10842  suplem1pr  11064  mulgt0sr  11117  ixxssixx  13414  difelfzle  13698  swrdnd0  14729  climrlim2  15636  qshash  15916  gcdcllem3  16595  vdwlem13  17089  ocvsscon  21889  opsrtoslem2  22273  txcnp  23847  t0kq  24045  filconn  24110  filuni  24112  alexsubALTlem3  24276  rectbntr0  25060  iscau4  25508  cfilres  25525  lmcau  25542  bcthlem2  25554  onvf1odlem2  35688  subfacp1lem6  35751  cvmsdisj  35836  meran1  37017  bj-bi3ant  37277  bj-cbv3ta  37516  bj-2upleq  37743  bj-ismooredr2  37847  bj-snmoore  37850  bj-isclm  38030  relowlssretop  38104  poimirlem30  38386  poimirlem31  38387  caushft  38498  partimeq  39647  ax13fromc9  39766  harinf  43862  ntrk0kbimka  44866  onfrALTlem3  45354  onfrALTlem2  45356  e222  45446  e111  45484  e333  45542  bitr3VD  45658  disjinfi  46011  prpair  48388  onsetrec  50621  aacllem  50759