Theorem sps 1563

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

Syntax hints:   → wi 4  ∀wal 1373

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

This theorem is referenced by:  19.21ht  1607  exim  1625  alexdc  1645  19.2  1664  ax10o  1741  hbae  1744  cbv1h  1772  equvini  1784  equveli  1785  ax10oe  1823  drex1  1824  drsb1  1825  exdistrfor  1826  ax11v2  1846  equs5or  1856  sbequi  1865  drsb2  1867  spsbim  1869  sbcomxyyz  2003  hbsb4t  2044  mopick  2136  eupickbi  2140  ceqsalg  2808  mo2icl  2962  reu6  2972  sbcal  3060  csbie2t  3153  dfss4st  3417  reldisj  3523  dfnfc2  3885  ssopab2  4343  eusvnfb  4522  mosubopt  4761  issref  5087  fv3  5626  fvmptt  5699  fnoprabg  6076  bj-exlimmp  16043  strcollnft  16257