Theorem sps 2226

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

Syntax hints:   → wi 4  ∀wal 1654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-12 2220

This theorem depends on definitions:  df-bi 199  df-ex 1879

This theorem is referenced by:  2sp  2227  19.2g  2229  nfim1  2239  axc16g  2290  axc11r  2388  axc15  2442  axc15OLD  2443  equvel  2477  dfsb2  2504  drsb1  2508  drsb2  2509  nfsb4t  2520  sbi1  2523  sbco2  2547  sbco3  2549  sb9  2558  sbal1  2593  eujustALT  2643  2eu6  2738  ralcom2  3314  ceqsalgALT  3448  reu6  3620  sbcal  3712  reldisj  4244  dfnfc2  4678  nfnid  5075  eusvnfb  5093  mosubopt  5196  dfid3  5251  idrefOLD  5751  fv3  6451  fvmptt  6547  fnoprabg  7021  wfrlem5  7685  pssnn  8447  kmlem16  9302  nd3  9726  axunndlem1  9732  axunnd  9733  axpowndlem1  9734  axregndlem1  9739  axregndlem2  9740  axacndlem5  9748  fundmpss  32195  frrlem5  32312  nalfal  32925  unisym1  32944  bj-sbsb  33341  bj-mo3OLD  33349  bj-ax9  33404  wl-nfimf1  33850  wl-dral1d  33855  wl-nfs1t  33861  wl-sb8t  33871  wl-sbhbt  33873  wl-equsb4  33876  wl-sbalnae  33882  wl-mo3t  33895  wl-ax11-lem5  33903  wl-ax11-lem8  33906  cotrintab  38755  pm11.57  39422  axc5c4c711toc7  39437  axc11next  39439  pm14.122b  39456  dropab1  39482  dropab2  39483  ax6e2eq  39594