Theorem sps 2179

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

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  2sp  2180  19.2g  2182  nfim1  2193  axc16g  2252  drsb2  2258  axc11r  2366  axc15  2422  equvel  2456  sb4a  2480  dfsb1  2481  dfsb2  2493  drsb1  2495  nfsb4t  2499  sbco2  2511  sbco3  2513  sb9  2519  sbal1  2528  sbal2  2529  eujustALT  2567  2eu6  2653  ralcom2  3374  ceqsalgALT  3508  reu6  3721  sbcal  3840  rexdifi  4144  reldisjOLD  4451  dfnfc2  4932  nfnid  5372  eusvnfb  5390  mosubopt  5509  dfid3  5576  fv3  6906  fvmptt  7014  fnoprabg  7526  fprlem1  8280  wfrlem5OLD  8308  pssnn  9164  pssnnOLD  9261  frrlem15  9748  kmlem16  10156  nd3  10580  axunndlem1  10586  axunnd  10587  axpowndlem1  10588  axregndlem1  10593  axregndlem2  10594  axacndlem5  10602  fundmpss  34676  nalfal  35226  unisym1  35246  bj-sbsb  35653  wl-nfimf1  36333  wl-axc11r  36337  wl-dral1d  36338  wl-nfs1t  36344  wl-sb8t  36355  wl-sbhbt  36357  wl-equsb4  36360  wl-sbalnae  36365  wl-2spsbbi  36368  wl-mo3t  36379  wl-ax11-lem5  36389  wl-ax11-lem8  36392  cotrintab  42298  pm11.57  43081  axc5c4c711toc7  43096  axc11next  43098  pm14.122b  43115  dropab1  43139  dropab2  43140  ax6e2eq  43251