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  1795  equvini  1807  equveli  1808  ax10oe  1846  drex1  1847  drsb1  1848  exdistrfor  1849  ax11v2  1869  equs5or  1879  sbequi  1888  drsb2  1890  spsbim  1892  sbcomxyyz  2028  hbsb4t  2069  mopick  2161  eupickbi  2165  ceqsalg  2844  mo2icl  2999  reu6  3009  sbcal  3097  csbie2t  3190  dfss4st  3458  reldisj  3564  dfnfc2  3937  ssopab2  4399  eusvnfb  4580  mosubopt  4820  issref  5150  fv3  5698  fvmptt  5774  fnoprabg  6162  bj-exlimmp  16653  strcollnft  16866