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  2284  ax13ALT  2454  r19.30  3129  intss2  5067  vtoclr  5713  funopg  6574  feldmfvelcdm  7086  abnex  7771  xpider  8809  undifixp  8962  onsdominel  9145  fodomr  9147  fodomfir  9319  wemaplem2  9541  rankuni2b  9867  infxpenlem  10092  dfac8b  10110  alephordi  10153  infdif  10286  cfflb  10337  alephval2  10657  tskxpss  10857  tskcard  10866  ingru  10900  grur1  10905  grothac  10915  suplem1pr  11137  mulgt0sr  11190  ixxssixx  13490  difelfzle  13775  swrdnd0  14807  climrlim2  15714  qshash  15994  gcdcllem3  16671  vdwlem13  17171  ocvsscon  21981  opsrtoslem2  22365  txcnp  23939  t0kq  24137  filconn  24202  filuni  24204  alexsubALTlem3  24368  rectbntr0  25152  iscau4  25600  cfilres  25617  lmcau  25634  bcthlem2  25646  onvf1odlem2  35925  subfacp1lem6  35992  cvmsdisj  36077  meran1  37241  bj-bi3ant  37501  bj-cbv3ta  37740  bj-2upleq  37967  bj-ismooredr2  38073  bj-snmoore  38076  bj-isclm  38255  relowlssretop  38329  poimirlem30  38611  poimirlem31  38612  caushft  38738  partimeq  39887  ax13fromc9  40006  harinf  44084  ntrk0kbimka  45082  onfrALTlem3  45570  onfrALTlem2  45572  e222  45662  e111  45700  e333  45758  bitr3VD  45874  disjinfi  46250  prpair  48626  onsetrec  50844  aacllem  50982