Theorem sps 2043

Description: Generalization of antecedent. (Contributed by NM, 5-Jan-1993.)

Hypothesis

Ref	Expression
sps.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
sps	⊢ (∀𝑥𝜑 → 𝜓)

Proof of Theorem sps

Step	Hyp	Ref	Expression
1		sp 2041	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
2		sps.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	syl 17	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  2sp  2044  19.2g  2046  nfim1  2055  axc16g  2119  axc11rvOLD  2125  axc11r  2175  axc15  2291  ax12v2OLD  2330  equvel  2335  dfsb2  2361  drsb1  2365  drsb2  2366  nfsb4t  2377  sbi1  2380  sbco2  2403  sbco3  2405  sb9  2414  sbal1  2448  eujustALT  2461  2eu6  2546  ralcom2  3083  ceqsalgALT  3204  reu6  3362  sbcal  3452  reldisj  3972  dfnfc2  4390  dfnfc2OLD  4391  eusvnfb  4788  nfnid  4823  mosubopt  4897  dfid3  4954  issref  5428  fv3  6116  fvmptt  6208  fnoprabg  6659  wfrlem5  7306  pssnn  8063  kmlem16  8870  nd3  9290  axunndlem1  9296  axunnd  9297  axpowndlem1  9298  axregndlem1  9303  axregndlem2  9304  axacndlem5  9312  fundmpss  30910  frrlem5  31028  nalf  31572  unisym1  31592  bj-sbsb  32012  bj-mo3OLD  32022  bj-xnex  32245  wl-nfimf1  32492  wl-dral1d  32497  wl-nfs1t  32503  wl-sb8t  32512  wl-sbhbt  32514  wl-equsb4  32517  wl-sbalnae  32524  wl-mo3t  32537  wl-ax11-lem5  32545  wl-ax11-lem8  32548  wl-sbcom3  32551  cotrintab  36940  pm11.57  37611  axc5c4c711toc7  37627  axc11next  37629  pm14.122b  37646  dropab1  37672  dropab2  37673  ax6e2eq  37794