Theorem sps 1535

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

Syntax hints:   → wi 4  ∀wal 1351

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

This theorem is referenced by:  19.21ht  1579  exim  1597  alexdc  1617  19.2  1636  ax10o  1713  hbae  1716  cbv1h  1744  equvini  1756  equveli  1757  ax10oe  1795  drex1  1796  drsb1  1797  exdistrfor  1798  ax11v2  1818  equs5or  1828  sbequi  1837  drsb2  1839  spsbim  1841  sbcomxyyz  1970  hbsb4t  2011  mopick  2102  eupickbi  2106  ceqsalg  2763  mo2icl  2914  reu6  2924  sbcal  3012  csbie2t  3103  dfss4st  3366  reldisj  3472  dfnfc2  3823  ssopab2  4269  eusvnfb  4448  mosubopt  4685  issref  5003  fv3  5530  fvmptt  5599  fnoprabg  5966  bj-exlimmp  14061  strcollnft  14276