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  2256  ax13ALT  2428  r19.30  3102  intss2  5039  vtoclr  5683  funopg  6521  feldmfvelcdm  7027  abnex  7700  xpider  8724  undifixp  8871  onsdominel  9053  fodomr  9055  fodomfir  9227  wemaplem2  9451  rankuni2b  9766  infxpenlem  9924  dfac8b  9942  ac10ct  9945  alephordi  9985  infdif  10119  cfflb  10170  alephval2  10484  tskxpss  10684  tskcard  10693  ingru  10727  grur1  10732  grothac  10742  suplem1pr  10964  mulgt0sr  11017  ixxssixx  13301  difelfzle  13584  swrdnd0  14609  climrlim2  15498  qshash  15779  gcdcllem3  16459  vdwlem13  16953  ocvsscon  21644  opsrtoslem2  22023  txcnp  23573  t0kq  23771  filconn  23836  filuni  23838  alexsubALTlem3  24002  rectbntr0  24786  iscau4  25234  cfilres  25251  lmcau  25268  bcthlem2  25280  onvf1odlem2  35274  subfacp1lem6  35355  cvmsdisj  35440  meran1  36581  bj-bi3ant  36842  bj-cbv3ta  37081  bj-2upleq  37307  bj-ismooredr2  37410  bj-snmoore  37413  bj-isclm  37593  relowlssretop  37667  poimirlem30  37959  poimirlem31  37960  caushft  38070  partimeq  39221  ax13fromc9  39340  harinf  43450  ntrk0kbimka  44454  onfrALTlem3  44959  onfrALTlem2  44961  e222  45051  e111  45089  e333  45147  bitr3VD  45263  disjinfi  45610  prpair  47949  onsetrec  50171  aacllem  50264