Theorem sps 2202

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

Syntax hints:   → wi 4  ∀wal 1630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196

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

This theorem is referenced by:  2sp  2203  19.2g  2205  nfim1  2214  axc16g  2281  axc11rvOLD  2287  axc11r  2332  axc15  2448  equvel  2484  dfsb2  2510  drsb1  2514  drsb2  2515  nfsb4t  2526  sbi1  2529  sbco2  2552  sbco3  2554  sb9  2563  sbal1  2597  eujustALT  2610  2eu6  2696  ralcom2  3242  ceqsalgALT  3371  reu6  3536  sbcal  3626  reldisj  4163  dfnfc2  4606  dfnfc2OLD  4607  eusvnfb  5011  nfnid  5046  mosubopt  5120  dfid3  5175  issref  5667  fv3  6367  fvmptt  6462  fnoprabg  6926  wfrlem5  7588  pssnn  8343  kmlem16  9179  nd3  9603  axunndlem1  9609  axunnd  9610  axpowndlem1  9611  axregndlem1  9616  axregndlem2  9617  axacndlem5  9625  fundmpss  31971  frrlem5  32090  nalf  32708  unisym1  32728  bj-sbsb  33130  bj-mo3OLD  33138  bj-ax9  33196  wl-nfimf1  33626  wl-dral1d  33631  wl-nfs1t  33637  wl-sb8t  33646  wl-sbhbt  33648  wl-equsb4  33651  wl-sbalnae  33658  wl-mo3t  33671  wl-ax11-lem5  33679  wl-ax11-lem8  33682  wl-sbcom3  33685  cotrintab  38423  pm11.57  39091  axc5c4c711toc7  39107  axc11next  39109  pm14.122b  39126  dropab1  39153  dropab2  39154  ax6e2eq  39275