Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 598. (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  2247  ax13ALT  2436  intss2  4993  vtoclr  5579  funopg  6358  abnex  7459  xpider  8351  undifixp  8481  onsdominel  8650  fodomr  8652  wemaplem2  8995  rankuni2b  9266  infxpenlem  9424  dfac8b  9442  ac10ct  9445  alephordi  9485  infdif  9620  cfflb  9670  alephval2  9983  tskxpss  10183  tskcard  10192  ingru  10226  grur1  10231  grothac  10241  suplem1pr  10463  mulgt0sr  10516  ixxssixx  12740  difelfzle  13015  swrdnd0  14010  climrlim2  14896  qshash  15174  gcdcllem3  15840  vdwlem13  16319  ocvsscon  20364  opsrtoslem2  20724  txcnp  22225  t0kq  22423  filconn  22488  filuni  22490  alexsubALTlem3  22654  rectbntr0  23437  iscau4  23883  cfilres  23900  lmcau  23917  bcthlem2  23929  subfacp1lem6  32545  cvmsdisj  32630  meran1  33872  bj-bi3ant  34036  bj-cbv3ta  34223  bj-2upleq  34448  bj-ismooredr2  34525  bj-snmoore  34528  bj-isclm  34705  relowlssretop  34780  poimirlem30  35087  poimirlem31  35088  caushft  35199  ax13fromc9  36202  harinf  39975  ntrk0kbimka  40742  onfrALTlem3  41250  onfrALTlem2  41252  e222  41342  e111  41380  e333  41439  bitr3VD  41555  disjinfi  41820  prpair  44018  onsetrec  45237  aacllem  45329