Theorem sps 2185

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 2183	. 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 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-12 2178

This theorem depends on definitions:  df-bi 210  df-ex 1787

This theorem is referenced by:  2sp  2186  19.2g  2188  nfim1  2200  axc16g  2260  drsb2  2266  axc11r  2367  axc15  2421  equvel  2455  sb1OLD  2482  sb4a  2484  dfsb1  2485  dfsb2  2497  drsb1  2499  nfsb4t  2503  sbco2  2515  sbco3  2517  sb9  2523  sbal1  2533  sbal2  2534  eujustALT  2573  2eu6  2659  ralcom2  3265  ceqsalgALT  3430  reu6  3623  sbcal  3740  rexdifi  4034  reldisjOLD  4339  dfnfc2  4817  nfnid  5239  eusvnfb  5257  mosubopt  5364  dfid3  5427  fv3  6686  fvmptt  6789  fnoprabg  7283  wfrlem5  7981  pssnn  8760  pssnnOLD  8808  kmlem16  9658  nd3  10082  axunndlem1  10088  axunnd  10089  axpowndlem1  10090  axregndlem1  10095  axregndlem2  10096  axacndlem5  10104  fundmpss  33304  fprlem1  33447  frrlem15  33452  nalfal  34222  unisym1  34242  bj-sbsb  34640  wl-nfimf1  35297  wl-axc11r  35301  wl-dral1d  35302  wl-nfs1t  35308  wl-sb8t  35319  wl-sbhbt  35321  wl-equsb4  35324  wl-sbalnae  35329  wl-2spsbbi  35332  wl-mo3t  35343  wl-ax11-lem5  35352  wl-ax11-lem8  35355  cotrintab  40751  pm11.57  41529  axc5c4c711toc7  41544  axc11next  41546  pm14.122b  41563  dropab1  41587  dropab2  41588  ax6e2eq  41699