Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 597. (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  2257  ax13ALT  2430  r19.30  3105  intss2  5051  vtoclr  5694  funopg  6533  feldmfvelcdm  7039  abnex  7711  xpider  8735  undifixp  8882  onsdominel  9064  fodomr  9066  fodomfir  9238  wemaplem2  9462  rankuni2b  9777  infxpenlem  9935  dfac8b  9953  ac10ct  9956  alephordi  9996  infdif  10130  cfflb  10181  alephval2  10495  tskxpss  10695  tskcard  10704  ingru  10738  grur1  10743  grothac  10753  suplem1pr  10975  mulgt0sr  11028  ixxssixx  13312  difelfzle  13595  swrdnd0  14620  climrlim2  15509  qshash  15790  gcdcllem3  16470  vdwlem13  16964  ocvsscon  21655  opsrtoslem2  22034  txcnp  23585  t0kq  23783  filconn  23848  filuni  23850  alexsubALTlem3  24014  rectbntr0  24798  iscau4  25246  cfilres  25263  lmcau  25280  bcthlem2  25292  onvf1odlem2  35286  subfacp1lem6  35367  cvmsdisj  35452  meran1  36593  bj-bi3ant  36854  bj-cbv3ta  37093  bj-2upleq  37319  bj-ismooredr2  37422  bj-snmoore  37425  bj-isclm  37605  relowlssretop  37679  poimirlem30  37971  poimirlem31  37972  caushft  38082  partimeq  39233  ax13fromc9  39352  harinf  43462  ntrk0kbimka  44466  onfrALTlem3  44971  onfrALTlem2  44973  e222  45063  e111  45101  e333  45159  bitr3VD  45275  disjinfi  45622  prpair  47955  onsetrec  50177  aacllem  50270