Theorem sps 2180

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

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

This theorem is referenced by:  2sp  2181  19.2g  2183  nfim1  2195  axc16g  2255  drsb2  2261  axc11r  2366  axc15  2422  equvel  2456  sb1OLD  2482  sb4a  2484  dfsb1  2485  dfsb2  2497  drsb1  2499  nfsb4t  2503  sbco2  2515  sbco3  2517  sb9  2523  sbal1  2533  sbal2  2534  eujustALT  2572  2eu6  2658  ralcom2  3288  ceqsalgALT  3455  reu6  3656  sbcal  3776  rexdifi  4076  reldisjOLD  4383  dfnfc2  4860  nfnid  5293  eusvnfb  5311  mosubopt  5418  dfid3  5483  fv3  6774  fvmptt  6877  fnoprabg  7375  fprlem1  8087  wfrlem5OLD  8115  pssnn  8913  pssnnOLD  8969  frrlem15  9446  kmlem16  9852  nd3  10276  axunndlem1  10282  axunnd  10283  axpowndlem1  10284  axregndlem1  10289  axregndlem2  10290  axacndlem5  10298  fundmpss  33646  nalfal  34519  unisym1  34539  bj-sbsb  34947  wl-nfimf1  35612  wl-axc11r  35616  wl-dral1d  35617  wl-nfs1t  35623  wl-sb8t  35634  wl-sbhbt  35636  wl-equsb4  35639  wl-sbalnae  35644  wl-2spsbbi  35647  wl-mo3t  35658  wl-ax11-lem5  35667  wl-ax11-lem8  35670  cotrintab  41111  pm11.57  41896  axc5c4c711toc7  41911  axc11next  41913  pm14.122b  41930  dropab1  41954  dropab2  41955  ax6e2eq  42066