Theorem sps 1498

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

Syntax hints:   → wi 4  ∀wal 1310

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

This theorem is referenced by:  19.21ht  1541  exim  1559  alexdc  1579  19.2  1598  ax10o  1674  hbae  1677  cbv1h  1704  equvini  1712  equveli  1713  ax10oe  1749  drex1  1750  drsb1  1751  exdistrfor  1752  ax11v2  1772  equs5or  1782  sbequi  1791  drsb2  1793  spsbim  1795  sbcomxyyz  1919  hbsb4t  1962  mopick  2051  eupickbi  2055  ceqsalg  2683  mo2icl  2830  reu6  2840  sbcal  2926  csbie2t  3012  dfss4st  3273  reldisj  3378  dfnfc2  3718  ssopab2  4155  eusvnfb  4333  mosubopt  4562  issref  4877  fv3  5396  fvmptt  5464  fnoprabg  5824  bj-exlimmp  12660  strcollnft  12865