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  2939  reu6  2949  sbcal  3037  csbie2t  3129  dfss4st  3392  reldisj  3498  dfnfc2  3853  ssopab2  4306  eusvnfb  4485  mosubopt  4724  issref  5048  fv3  5577  fvmptt  5649  fnoprabg  6019  bj-exlimmp  15261  strcollnft  15476