Theorem sps 1525

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

Syntax hints:   → wi 4  ∀wal 1341

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

This theorem is referenced by:  19.21ht  1569  exim  1587  alexdc  1607  19.2  1626  ax10o  1703  hbae  1706  cbv1h  1734  equvini  1746  equveli  1747  ax10oe  1785  drex1  1786  drsb1  1787  exdistrfor  1788  ax11v2  1808  equs5or  1818  sbequi  1827  drsb2  1829  spsbim  1831  sbcomxyyz  1960  hbsb4t  2001  mopick  2092  eupickbi  2096  ceqsalg  2754  mo2icl  2905  reu6  2915  sbcal  3002  csbie2t  3093  dfss4st  3355  reldisj  3460  dfnfc2  3807  ssopab2  4253  eusvnfb  4432  mosubopt  4669  issref  4986  fv3  5509  fvmptt  5577  fnoprabg  5943  bj-exlimmp  13660  strcollnft  13876