Theorem sps 2184

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-ex 1781

This theorem is referenced by:  2sp  2185  19.2g  2187  nfim1  2199  axc16g  2261  drsb2  2267  axc11r  2386  axc15  2444  equvel  2479  sb1OLD  2507  sb4a  2509  dfsb1  2510  dfsb2  2532  drsb1  2535  nfsb4t  2539  sbi1OLD  2542  sbco2  2553  sbco3  2555  sb9  2561  sbal1  2572  sbal2  2573  dfsb2ALT  2591  nfsb4tALT  2604  sbi1ALT  2606  sbco2ALT  2615  eujustALT  2657  2eu6  2742  ralcom2  3365  ceqsalgALT  3532  reu6  3719  sbcal  3835  rexdifi  4124  reldisj  4404  dfnfc2  4862  nfnid  5278  eusvnfb  5296  mosubopt  5402  dfid3  5464  fv3  6690  fvmptt  6790  fnoprabg  7277  wfrlem5  7961  pssnn  8738  kmlem16  9593  nd3  10013  axunndlem1  10019  axunnd  10020  axpowndlem1  10021  axregndlem1  10026  axregndlem2  10027  axacndlem5  10035  fundmpss  33011  fprlem1  33139  frrlem15  33144  nalfal  33753  unisym1  33773  bj-sbsb  34162  bj-ax9  34218  wl-nfimf1  34768  wl-axc11r  34772  wl-dral1d  34773  wl-nfs1t  34779  wl-sb8t  34790  wl-sbhbt  34792  wl-equsb4  34795  wl-sbalnae  34800  wl-2spsbbi  34803  wl-mo3t  34814  wl-ax11-lem5  34823  wl-ax11-lem8  34826  cotrintab  39981  pm11.57  40728  axc5c4c711toc7  40743  axc11next  40745  pm14.122b  40762  dropab1  40786  dropab2  40787  ax6e2eq  40898