Theorem sps 2053

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 2051	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
2		sps.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	syl 17	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044

This theorem depends on definitions:  df-bi 197  df-ex 1702

This theorem is referenced by:  2sp  2054  19.2g  2056  nfim1  2065  axc16g  2130  axc11rvOLD  2136  axc11r  2186  axc15  2302  ax12v2OLD  2341  equvel  2346  dfsb2  2372  drsb1  2376  drsb2  2377  nfsb4t  2388  sbi1  2391  sbco2  2414  sbco3  2416  sb9  2425  sbal1  2459  eujustALT  2472  2eu6  2557  ralcom2  3098  ceqsalgALT  3221  reu6  3382  sbcal  3472  reldisj  3998  dfnfc2  4427  dfnfc2OLD  4428  eusvnfb  4832  nfnid  4867  mosubopt  4942  dfid3  5000  issref  5478  fv3  6173  fvmptt  6266  fnoprabg  6726  abnex  6929  wfrlem5  7379  pssnn  8138  kmlem16  8947  nd3  9371  axunndlem1  9377  axunnd  9378  axpowndlem1  9379  axregndlem1  9384  axregndlem2  9385  axacndlem5  9393  fundmpss  31421  frrlem5  31538  nalf  32097  unisym1  32117  bj-sbsb  32520  bj-mo3OLD  32530  bj-ax9  32590  wl-nfimf1  32984  wl-dral1d  32989  wl-nfs1t  32995  wl-sb8t  33004  wl-sbhbt  33006  wl-equsb4  33009  wl-sbalnae  33016  wl-mo3t  33029  wl-ax11-lem5  33037  wl-ax11-lem8  33040  wl-sbcom3  33043  cotrintab  37441  pm11.57  38110  axc5c4c711toc7  38126  axc11next  38128  pm14.122b  38145  dropab1  38172  dropab2  38173  ax6e2eq  38294