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 ⊢ (𝜑 → (𝜒 → 𝜏))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl2imc  42  sylc  66  sbequ2  2284  ax13ALT  2456  r19.30  3131  intss2  5073  vtoclr  5723  funopg  6570  feldmfvelcdm  7081  abnex  7754  xpider  8784  undifixp  8930  onsdominel  9112  fodomr  9114  fodomfir  9285  wemaplem2  9507  rankuni2b  9823  infxpenlem  10004  dfac8b  10022  alephordi  10065  infdif  10198  cfflb  10249  alephval2  10563  tskxpss  10763  tskcard  10772  ingru  10806  grur1  10811  grothac  10821  suplem1pr  11043  mulgt0sr  11096  ixxssixx  13392  difelfzle  13676  swrdnd0  14702  climrlim2  15605  qshash  15886  gcdcllem3  16565  vdwlem13  17059  ocvsscon  21836  opsrtoslem2  22218  txcnp  23788  t0kq  23986  filconn  24051  filuni  24053  alexsubALTlem3  24217  rectbntr0  25001  iscau4  25449  cfilres  25466  lmcau  25483  bcthlem2  25495  onvf1odlem2  35596  subfacp1lem6  35685  cvmsdisj  35770  meran1  36950  bj-bi3ant  37210  bj-cbv3ta  37449  bj-2upleq  37676  bj-ismooredr2  37780  bj-snmoore  37783  bj-isclm  37963  relowlssretop  38037  poimirlem30  38329  poimirlem31  38330  caushft  38440  partimeq  39589  ax13fromc9  39708  harinf  43789  ntrk0kbimka  44793  onfrALTlem3  45281  onfrALTlem2  45283  e222  45373  e111  45411  e333  45469  bitr3VD  45585  disjinfi  45938  prpair  48278  onsetrec  50514  aacllem  50649