Theorem syl2im 39

Description: Replace two antecedents. Implication-only version of syl2an 493. (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 33	. 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  40  sylc  63  axc16gOLD  2147  ax13OLD  2293  vtoclr  5086  funopg  5836  xpider  7705  undifixp  7830  onsdominel  7994  fodomr  7996  wemaplem2  8335  rankuni2b  8599  infxpenlem  8719  dfac8b  8737  ac10ct  8740  alephordi  8780  infdif  8914  cfflb  8964  alephval2  9273  tskxpss  9473  tskcard  9482  ingru  9516  grur1  9521  grothac  9531  suplem1pr  9753  mulgt0sr  9805  ixxssixx  12060  difelfzle  12321  climrlim2  14126  qshash  14398  gcdcllem3  15061  vdwlem13  15535  opsrtoslem2  19306  ocvsscon  19838  txcnp  21233  t0kq  21431  filcon  21497  filuni  21499  alexsubALTlem3  21663  rectbntr0  22443  iscau4  22885  cfilres  22902  lmcau  22919  bcthlem2  22930  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  clwlkfoclwwlk  26372  subfacp1lem6  30421  cvmsdisj  30506  meran1  31580  bj-bi3ant  31747  bj-cbv3ta  31897  bj-2upleq  32193  relowlssretop  32387  poimirlem30  32609  poimirlem31  32610  caushft  32727  ax13fromc9  33209  harinf  36619  ntrk0kbimka  37357  onfrALTlem3  37780  onfrALTlem2  37782  e222  37882  e111  37920  e333  37981  bitr3VD  38106  clwlksfoclwwlk  41270  onsetrec  42250  aacllem  42356