Theorem sps 2193

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 2191	. 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

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

This theorem is referenced by:  2sp  2194  19.2g  2196  nfim1  2207  axc16g  2268  drsb2  2274  axc11r  2372  axc15  2426  equvel  2460  sb4a  2484  dfsb1  2485  dfsb2  2497  drsb1  2499  nfsb4t  2503  sbco2  2515  sbco3  2517  sb9  2523  sbal1  2532  sbal2  2533  eujustALT  2572  2eu6  2657  ralcom2  3339  ceqsalgALT  3466  reu6  3672  rexdifi  4090  dfnfc2  4872  nfnid  5317  eusvnfb  5335  mosubopt  5464  dfid3  5529  fv3  6858  fvmptt  6968  fnoprabg  7490  fprlem1  8250  pssnn  9103  frrlem15  9681  kmlem16  10088  nd3  10512  axunndlem1  10518  axunnd  10519  axpowndlem1  10520  axregndlem1  10525  axregndlem2  10526  axacndlem5  10534  axsepg2  35225  axsepg2ALT  35226  axnulg  35251  fundmpss  35949  nalfal  36585  unisym1  36605  axtcond  36660  bj-sbsb  37144  wl-nfimf1  37851  wl-axc11r  37855  wl-dral1d  37856  wl-nfs1t  37862  wl-sb8t  37877  wl-sbhbt  37879  wl-equsb4  37882  wl-sbalnae  37887  wl-2spsbbi  37890  wl-mo3t  37901  cotrintab  44041  pm11.57  44816  axc5c4c711toc7  44831  axc11next  44833  pm14.122b  44850  dropab1  44873  dropab2  44874  ax6e2eq  44984  quantgodelALT  47303