Theorem sps 1430

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

Syntax hints:   → wi 4  ∀wal 1241

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

This theorem is referenced by:  19.21ht  1473  exim  1490  alexdc  1510  19.2  1529  ax10o  1603  hbae  1606  cbv1h  1633  equvini  1641  equveli  1642  ax10oe  1678  drex1  1679  drsb1  1680  exdistrfor  1681  ax11v2  1701  equs5or  1711  sbequi  1720  drsb2  1722  spsbim  1724  sbcomxyyz  1846  hbsb4t  1889  mopick  1978  eupickbi  1982  ceqsalg  2582  mo2icl  2720  reu6  2730  sbcal  2810  csbie2t  2894  reldisj  3271  dfnfc2  3598  ssopab2  4012  eusvnfb  4186  mosubopt  4405  issref  4707  fv3  5197  fvmptt  5262  fnoprabg  5602  bj-exlimmp  9909  strcollnft  10109