Theorem sps 1470

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

Syntax hints:   → wi 4  ∀wal 1282

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

This theorem is referenced by:  19.21ht  1513  exim  1530  alexdc  1550  19.2  1569  ax10o  1643  hbae  1646  cbv1h  1673  equvini  1681  equveli  1682  ax10oe  1718  drex1  1719  drsb1  1720  exdistrfor  1721  ax11v2  1741  equs5or  1751  sbequi  1760  drsb2  1762  spsbim  1764  sbcomxyyz  1887  hbsb4t  1930  mopick  2019  eupickbi  2023  ceqsalg  2627  mo2icl  2771  reu6  2781  sbcal  2865  csbie2t  2950  reldisj  3295  dfnfc2  3619  ssopab2  4030  eusvnfb  4204  mosubopt  4423  issref  4727  fv3  5218  fvmptt  5283  fnoprabg  5622  bj-exlimmp  10580  strcollnft  10779