Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 594. (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  2236  ax13ALT  2418  r19.30  3109  intss2  5112  vtoclr  5741  funopg  6588  feldmfvelcdm  7095  abnex  7760  xpider  8807  undifixp  8953  onsdominel  9154  fodomr  9156  wemaplem2  9577  rankuni2b  9883  infxpenlem  10043  dfac8b  10061  ac10ct  10064  alephordi  10104  infdif  10239  cfflb  10289  alephval2  10602  tskxpss  10802  tskcard  10811  ingru  10845  grur1  10850  grothac  10860  suplem1pr  11082  mulgt0sr  11135  ixxssixx  13378  difelfzle  13654  swrdnd0  14651  climrlim2  15535  qshash  15817  gcdcllem3  16487  vdwlem13  16981  ocvsscon  21641  opsrtoslem2  22039  txcnp  23585  t0kq  23783  filconn  23848  filuni  23850  alexsubALTlem3  24014  rectbntr0  24809  iscau4  25268  cfilres  25285  lmcau  25302  bcthlem2  25314  subfacp1lem6  34946  cvmsdisj  35031  meran1  36046  bj-bi3ant  36217  bj-cbv3ta  36414  bj-2upleq  36642  bj-ismooredr2  36740  bj-snmoore  36743  bj-isclm  36921  relowlssretop  36993  poimirlem30  37274  poimirlem31  37275  caushft  37385  partimeq  38431  ax13fromc9  38528  harinf  42602  ntrk0kbimka  43616  onfrALTlem3  44130  onfrALTlem2  44132  e222  44222  e111  44260  e333  44319  bitr3VD  44435  disjinfi  44709  prpair  46983  onsetrec  48330  aacllem  48425