Theorem sps 1548

Description: Generalization of antecedent. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
sps.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
sps	⊢ (∀𝑥𝜑 → 𝜓)

Proof of Theorem sps

Step	Hyp	Ref	Expression
1		sp 1522	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
2		sps.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	syl 14	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1521

This theorem is referenced by:  19.21ht  1592  exim  1610  alexdc  1630  19.2  1649  ax10o  1726  hbae  1729  cbv1h  1757  equvini  1769  equveli  1770  ax10oe  1808  drex1  1809  drsb1  1810  exdistrfor  1811  ax11v2  1831  equs5or  1841  sbequi  1850  drsb2  1852  spsbim  1854  sbcomxyyz  1988  hbsb4t  2029  mopick  2120  eupickbi  2124  ceqsalg  2788  mo2icl  2940  reu6  2950  sbcal  3038  csbie2t  3130  dfss4st  3393  reldisj  3499  dfnfc2  3854  ssopab2  4307  eusvnfb  4486  mosubopt  4725  issref  5049  fv3  5578  fvmptt  5650  fnoprabg  6020  bj-exlimmp  15331  strcollnft  15546