Theorem syl2im 41

Description: Replace two antecedents. Implication-only version of syl2an 608. (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  2288  ax13ALT  2457  r19.30  3133  intss2  5071  vtoclr  5718  funopg  6594  feldmfvelcdm  7110  abnex  7795  xpider  8837  undifixp  8990  onsdominel  9173  fodomr  9175  fodomfir  9347  wemaplem2  9568  rankuni2b  9894  infxpenlem  10119  dfac8b  10137  alephordi  10180  infdif  10313  cfflb  10364  alephval2  10684  tskxpss  10884  tskcard  10893  ingru  10927  grur1  10932  grothac  10942  suplem1pr  11164  mulgt0sr  11217  ixxssixx  13517  difelfzle  13802  swrdnd0  14835  climrlim2  15743  qshash  16023  gcdcllem3  16700  vdwlem13  17200  ocvsscon  22011  opsrtoslem2  22395  txcnp  23969  t0kq  24167  filconn  24232  filuni  24234  alexsubALTlem3  24398  rectbntr0  25182  iscau4  25630  cfilres  25647  lmcau  25664  bcthlem2  25676  onvf1odlem2  36032  subfacp1lem6  36117  cvmsdisj  36202  meran1  37377  bj-bi3ant  37637  bj-cbv3ta  37876  bj-2upleq  38103  bj-ismooredr2  38222  bj-snmoore  38225  bj-isclm  38404  relowlssretop  38478  poimirlem30  38760  poimirlem31  38761  caushft  38887  partimeq  40036  ax13fromc9  40155  harinf  44234  ntrk0kbimka  45231  onfrALTlem3  45718  onfrALTlem2  45720  e222  45810  e111  45848  e333  45906  bitr3VD  46022  disjinfi  46412  prpair  48788  onsetrec  51081  aacllem  51219