Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 597. (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  2250  ax13ALT  2447  vtoclr  5615  funopg  6389  abnex  7479  xpider  8368  undifixp  8498  onsdominel  8666  fodomr  8668  wemaplem2  9011  rankuni2b  9282  infxpenlem  9439  dfac8b  9457  ac10ct  9460  alephordi  9500  infdif  9631  cfflb  9681  alephval2  9994  tskxpss  10194  tskcard  10203  ingru  10237  grur1  10242  grothac  10252  suplem1pr  10474  mulgt0sr  10527  ixxssixx  12753  difelfzle  13021  swrdnd0  14019  climrlim2  14904  qshash  15182  gcdcllem3  15850  vdwlem13  16329  opsrtoslem2  20265  ocvsscon  20819  txcnp  22228  t0kq  22426  filconn  22491  filuni  22493  alexsubALTlem3  22657  rectbntr0  23440  iscau4  23882  cfilres  23899  lmcau  23916  bcthlem2  23928  subfacp1lem6  32432  cvmsdisj  32517  meran1  33759  bj-bi3ant  33923  bj-cbv3ta  34108  bj-2upleq  34327  bj-intss  34394  bj-ismooredr2  34405  bj-snmoore  34408  bj-isclm  34575  relowlssretop  34647  poimirlem30  34937  poimirlem31  34938  caushft  35051  ax13fromc9  36057  harinf  39651  ntrk0kbimka  40409  onfrALTlem3  40898  onfrALTlem2  40900  e222  40990  e111  41028  e333  41087  bitr3VD  41203  prpair  43683  onsetrec  44830  aacllem  44922