Theorem sps 1530

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

Syntax hints:   → wi 4  ∀wal 1346

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

This theorem is referenced by:  19.21ht  1574  exim  1592  alexdc  1612  19.2  1631  ax10o  1708  hbae  1711  cbv1h  1739  equvini  1751  equveli  1752  ax10oe  1790  drex1  1791  drsb1  1792  exdistrfor  1793  ax11v2  1813  equs5or  1823  sbequi  1832  drsb2  1834  spsbim  1836  sbcomxyyz  1965  hbsb4t  2006  mopick  2097  eupickbi  2101  ceqsalg  2758  mo2icl  2909  reu6  2919  sbcal  3006  csbie2t  3097  dfss4st  3360  reldisj  3466  dfnfc2  3814  ssopab2  4260  eusvnfb  4439  mosubopt  4676  issref  4993  fv3  5519  fvmptt  5587  fnoprabg  5954  bj-exlimmp  13804  strcollnft  14019