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  2373  axc15  2427  equvel  2461  sb4a  2485  dfsb1  2486  dfsb2  2498  drsb1  2500  nfsb4t  2504  sbco2  2516  sbco3  2518  sb9  2524  sbal1  2533  sbal2  2534  eujustALT  2573  2eu6  2658  ralcom2  3340  ceqsalgALT  3467  reu6  3673  rexdifi  4091  dfnfc2  4873  nfnid  5312  eusvnfb  5330  mosubopt  5458  dfid3  5522  fv3  6852  fvmptt  6962  fnoprabg  7483  fprlem1  8243  pssnn  9096  frrlem15  9672  kmlem16  10079  nd3  10503  axunndlem1  10509  axunnd  10510  axpowndlem1  10511  axregndlem1  10516  axregndlem2  10517  axacndlem5  10525  axsepg2  35241  axsepg2ALT  35242  axnulg  35267  fundmpss  35965  nalfal  36601  unisym1  36621  axtcond  36676  bj-sbsb  37160  wl-nfimf1  37865  wl-axc11r  37869  wl-dral1d  37870  wl-nfs1t  37876  wl-sb8t  37891  wl-sbhbt  37893  wl-equsb4  37896  wl-sbalnae  37901  wl-2spsbbi  37904  wl-mo3t  37915  cotrintab  44059  pm11.57  44834  axc5c4c711toc7  44849  axc11next  44851  pm14.122b  44868  dropab1  44891  dropab2  44892  ax6e2eq  45002