Theorem syl2im 41

Description: Replace two antecedents. Implication-only version of syl2an 607. (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 ⊢ (𝜑 → (𝜒 → 𝜏))

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  42  sylc  66  sbequ2  2283  ax13ALT  2455  r19.30  3130  intss2  5073  vtoclr  5724  funopg  6570  feldmfvelcdm  7081  abnex  7755  xpider  8785  undifixp  8931  onsdominel  9113  fodomr  9115  fodomfir  9286  wemaplem2  9508  rankuni2b  9824  infxpenlem  9996  dfac8b  10014  ac10ct  10017  alephordi  10057  infdif  10190  cfflb  10242  alephval2  10556  tskxpss  10756  tskcard  10765  ingru  10799  grur1  10804  grothac  10814  suplem1pr  11036  mulgt0sr  11089  ixxssixx  13385  difelfzle  13668  swrdnd0  14694  climrlim2  15597  qshash  15878  gcdcllem3  16558  vdwlem13  17052  ocvsscon  21804  opsrtoslem2  22186  txcnp  23756  t0kq  23954  filconn  24019  filuni  24021  alexsubALTlem3  24185  rectbntr0  24969  iscau4  25417  cfilres  25434  lmcau  25451  bcthlem2  25463  onvf1odlem2  35542  subfacp1lem6  35631  cvmsdisj  35716  meran1  36866  bj-bi3ant  37126  bj-cbv3ta  37365  bj-2upleq  37592  bj-ismooredr2  37696  bj-snmoore  37699  bj-isclm  37879  relowlssretop  37953  poimirlem30  38245  poimirlem31  38246  caushft  38356  partimeq  39507  ax13fromc9  39626  harinf  43709  ntrk0kbimka  44713  onfrALTlem3  45201  onfrALTlem2  45203  e222  45293  e111  45331  e333  45389  bitr3VD  45505  disjinfi  45858  prpair  48195  onsetrec  50431  aacllem  50546