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  2250  ax13ALT  2424  r19.30  3101  intss2  5074  vtoclr  5703  funopg  6552  feldmfvelcdm  7060  abnex  7735  xpider  8763  undifixp  8909  onsdominel  9095  fodomr  9097  fodomfir  9285  wemaplem2  9506  rankuni2b  9812  infxpenlem  9972  dfac8b  9990  ac10ct  9993  alephordi  10033  infdif  10167  cfflb  10218  alephval2  10531  tskxpss  10731  tskcard  10740  ingru  10774  grur1  10779  grothac  10789  suplem1pr  11011  mulgt0sr  11064  ixxssixx  13326  difelfzle  13608  swrdnd0  14628  climrlim2  15519  qshash  15799  gcdcllem3  16477  vdwlem13  16970  ocvsscon  21590  opsrtoslem2  21969  txcnp  23513  t0kq  23711  filconn  23776  filuni  23778  alexsubALTlem3  23942  rectbntr0  24727  iscau4  25185  cfilres  25202  lmcau  25219  bcthlem2  25231  subfacp1lem6  35172  cvmsdisj  35257  meran1  36394  bj-bi3ant  36572  bj-cbv3ta  36769  bj-2upleq  36995  bj-ismooredr2  37093  bj-snmoore  37096  bj-isclm  37274  relowlssretop  37346  poimirlem30  37639  poimirlem31  37640  caushft  37750  partimeq  38796  ax13fromc9  38894  harinf  43016  ntrk0kbimka  44021  onfrALTlem3  44527  onfrALTlem2  44529  e222  44619  e111  44657  e333  44715  bitr3VD  44831  disjinfi  45179  prpair  47492  onsetrec  49687  aacllem  49780