Theorem sps 1586

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

Syntax hints:   → wi 4  ∀wal 1396

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

This theorem is referenced by:  19.21ht  1630  exim  1648  alexdc  1668  19.2  1687  ax10o  1763  hbae  1766  cbv1h  1794  equvini  1806  equveli  1807  ax10oe  1845  drex1  1846  drsb1  1847  exdistrfor  1848  ax11v2  1868  equs5or  1878  sbequi  1887  drsb2  1889  spsbim  1891  sbcomxyyz  2025  hbsb4t  2066  mopick  2158  eupickbi  2162  ceqsalg  2832  mo2icl  2986  reu6  2996  sbcal  3084  csbie2t  3177  dfss4st  3442  reldisj  3548  dfnfc2  3916  ssopab2  4376  eusvnfb  4557  mosubopt  4797  issref  5126  fv3  5671  fvmptt  5747  fnoprabg  6132  bj-exlimmp  16467  strcollnft  16680