Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 604. (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  sbi1lem  2092  sbequ2  2274  ax13ALT  2446  r19.30  3119  intss2  5055  vtoclr  5699  funopg  6540  feldmfvelcdm  7052  abnex  7725  xpider  8754  undifixp  8901  onsdominel  9083  fodomr  9085  fodomfir  9257  wemaplem2  9481  rankuni2b  9797  infxpenlem  9955  dfac8b  9973  ac10ct  9976  alephordi  10016  infdif  10150  cfflb  10202  alephval2  10516  tskxpss  10716  tskcard  10725  ingru  10759  grur1  10764  grothac  10774  suplem1pr  10996  mulgt0sr  11049  ixxssixx  13349  difelfzle  13632  swrdnd0  14657  climrlim2  15546  qshash  15827  gcdcllem3  16507  vdwlem13  17001  ocvsscon  21696  opsrtoslem2  22078  txcnp  23649  t0kq  23847  filconn  23912  filuni  23914  alexsubALTlem3  24078  rectbntr0  24862  iscau4  25310  cfilres  25327  lmcau  25344  bcthlem2  25356  onvf1odlem2  35392  subfacp1lem6  35473  cvmsdisj  35558  meran1  36709  bj-bi3ant  36970  bj-cbv3ta  37209  bj-2upleq  37435  bj-ismooredr2  37538  bj-snmoore  37541  bj-isclm  37721  relowlssretop  37795  poimirlem30  38087  poimirlem31  38088  caushft  38198  partimeq  39349  ax13fromc9  39468  harinf  43549  ntrk0kbimka  44553  onfrALTlem3  45058  onfrALTlem2  45060  e222  45150  e111  45188  e333  45246  bitr3VD  45362  disjinfi  45708  prpair  48045  onsetrec  50267  aacllem  50360