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  3349  ceqsalgALT  3479  reu6  3686  rexdifi  4104  dfnfc2  4887  nfnid  5322  eusvnfb  5340  mosubopt  5466  dfid3  5530  fv3  6860  fvmptt  6970  fnoprabg  7491  fprlem1  8252  pssnn  9105  frrlem15  9681  kmlem16  10088  nd3  10512  axunndlem1  10518  axunnd  10519  axpowndlem1  10520  axregndlem1  10525  axregndlem2  10526  axacndlem5  10534  axsepg2  35257  axsepg2ALT  35258  axnulg  35283  fundmpss  35980  nalfal  36616  unisym1  36636  bj-sbsb  37079  wl-nfimf1  37775  wl-axc11r  37779  wl-dral1d  37780  wl-nfs1t  37786  wl-sb8t  37801  wl-sbhbt  37803  wl-equsb4  37806  wl-sbalnae  37811  wl-2spsbbi  37814  wl-mo3t  37825  cotrintab  43964  pm11.57  44739  axc5c4c711toc7  44754  axc11next  44756  pm14.122b  44773  dropab1  44796  dropab2  44797  ax6e2eq  44907