Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 596. (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  2249  ax13ALT  2429  r19.30  3107  intss2  5084  vtoclr  5717  funopg  6569  feldmfvelcdm  7075  abnex  7749  xpider  8800  undifixp  8946  onsdominel  9138  fodomr  9140  fodomfir  9338  wemaplem2  9559  rankuni2b  9865  infxpenlem  10025  dfac8b  10043  ac10ct  10046  alephordi  10086  infdif  10220  cfflb  10271  alephval2  10584  tskxpss  10784  tskcard  10793  ingru  10827  grur1  10832  grothac  10842  suplem1pr  11064  mulgt0sr  11117  ixxssixx  13374  difelfzle  13656  swrdnd0  14673  climrlim2  15561  qshash  15841  gcdcllem3  16518  vdwlem13  17011  ocvsscon  21633  opsrtoslem2  22012  txcnp  23556  t0kq  23754  filconn  23819  filuni  23821  alexsubALTlem3  23985  rectbntr0  24770  iscau4  25229  cfilres  25246  lmcau  25263  bcthlem2  25275  subfacp1lem6  35153  cvmsdisj  35238  meran1  36375  bj-bi3ant  36553  bj-cbv3ta  36750  bj-2upleq  36976  bj-ismooredr2  37074  bj-snmoore  37077  bj-isclm  37255  relowlssretop  37327  poimirlem30  37620  poimirlem31  37621  caushft  37731  partimeq  38773  ax13fromc9  38870  harinf  43005  ntrk0kbimka  44010  onfrALTlem3  44517  onfrALTlem2  44519  e222  44609  e111  44647  e333  44705  bitr3VD  44821  disjinfi  45164  prpair  47463  onsetrec  49520  aacllem  49613