Theorem sps 2183

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-ex 1777

This theorem is referenced by:  2sp  2184  19.2g  2186  nfim1  2197  axc16g  2258  drsb2  2264  axc11r  2369  axc15  2425  equvel  2459  sb4a  2483  dfsb1  2484  dfsb2  2496  drsb1  2498  nfsb4t  2502  sbco2  2514  sbco3  2516  sb9  2522  sbal1  2531  sbal2  2532  eujustALT  2570  2eu6  2655  ralcom2  3375  ceqsalgALT  3516  reu6  3735  sbcal  3855  rexdifi  4160  dfnfc2  4934  nfnid  5381  eusvnfb  5399  mosubopt  5520  dfid3  5586  fv3  6925  fvmptt  7036  fnoprabg  7556  fprlem1  8324  wfrlem5OLD  8352  pssnn  9207  frrlem15  9795  kmlem16  10204  nd3  10627  axunndlem1  10633  axunnd  10634  axpowndlem1  10635  axregndlem1  10640  axregndlem2  10641  axacndlem5  10649  axsepg2  35075  axsepg2ALT  35076  axnulg  35085  fundmpss  35748  nalfal  36386  unisym1  36406  bj-sbsb  36820  wl-nfimf1  37507  wl-axc11r  37511  wl-dral1d  37512  wl-nfs1t  37518  wl-sb8t  37533  wl-sbhbt  37535  wl-equsb4  37538  wl-sbalnae  37543  wl-2spsbbi  37546  wl-mo3t  37557  wl-ax11-lem5  37570  wl-ax11-lem8  37573  cotrintab  43604  pm11.57  44385  axc5c4c711toc7  44400  axc11next  44402  pm14.122b  44419  dropab1  44443  dropab2  44444  ax6e2eq  44555