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  5710  funopg  6562  feldmfvelcdm  7074  abnex  7754  xpider  8787  undifixp  8940  onsdominel  9123  fodomr  9125  fodomfir  9297  wemaplem2  9519  rankuni2b  9840  infxpenlem  10063  dfac8b  10081  alephordi  10124  infdif  10257  cfflb  10308  alephval2  10628  tskxpss  10828  tskcard  10837  ingru  10871  grur1  10876  grothac  10886  suplem1pr  11108  mulgt0sr  11161  ixxssixx  13459  difelfzle  13743  swrdnd0  14774  climrlim2  15681  qshash  15961  gcdcllem3  16638  vdwlem13  17132  ocvsscon  21942  opsrtoslem2  22326  txcnp  23900  t0kq  24098  filconn  24163  filuni  24165  alexsubALTlem3  24329  rectbntr0  25113  iscau4  25561  cfilres  25578  lmcau  25595  bcthlem2  25607  onvf1odlem2  35808  subfacp1lem6  35871  cvmsdisj  35956  meran1  37121  bj-bi3ant  37381  bj-cbv3ta  37620  bj-2upleq  37847  bj-ismooredr2  37951  bj-snmoore  37954  bj-isclm  38132  relowlssretop  38206  poimirlem30  38488  poimirlem31  38489  caushft  38615  partimeq  39764  ax13fromc9  39883  harinf  43979  ntrk0kbimka  44983  onfrALTlem3  45471  onfrALTlem2  45473  e222  45563  e111  45601  e333  45659  bitr3VD  45775  disjinfi  46128  prpair  48505  onsetrec  50723  aacllem  50861