Theorem sps 1590

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

Syntax hints:   → wi 4  ∀wal 1400

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

This theorem is referenced by:  19.21ht  1634  exim  1652  alexdc  1672  19.2  1691  ax10o  1767  hbae  1770  cbv1h  1799  equvini  1811  equveli  1812  ax10oe  1850  drex1  1851  drsb1  1852  exdistrfor  1853  ax11v2  1873  equs5or  1883  sbequi  1892  drsb2  1894  spsbim  1896  sbcomxyyz  2032  hbsb4t  2073  mopick  2165  eupickbi  2169  ceqsalg  2850  mo2icl  3005  reu6  3015  sbcal  3103  csbie2t  3196  dfss4st  3464  reldisj  3576  dfnfc2  3951  ssopab2  4416  eusvnfb  4598  mosubopt  4838  issref  5168  fv3  5716  fvmptt  5794  fnoprabg  6183  bj-exlimmp  16780  strcollnft  16993