Theorem sps 1561

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

Syntax hints:   → wi 4  ∀wal 1371

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

This theorem is referenced by:  19.21ht  1605  exim  1623  alexdc  1643  19.2  1662  ax10o  1739  hbae  1742  cbv1h  1770  equvini  1782  equveli  1783  ax10oe  1821  drex1  1822  drsb1  1823  exdistrfor  1824  ax11v2  1844  equs5or  1854  sbequi  1863  drsb2  1865  spsbim  1867  sbcomxyyz  2001  hbsb4t  2042  mopick  2133  eupickbi  2137  ceqsalg  2801  mo2icl  2953  reu6  2963  sbcal  3051  csbie2t  3143  dfss4st  3407  reldisj  3513  dfnfc2  3870  ssopab2  4326  eusvnfb  4505  mosubopt  4744  issref  5070  fv3  5606  fvmptt  5678  fnoprabg  6053  bj-exlimmp  15779  strcollnft  15994