Theorem sps 1754

Description: Generalization of antecedent. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
sps.1	⊢ (φ → ψ)

Assertion

Ref	Expression
sps	⊢ (∀xφ → ψ)

Proof of Theorem sps

Step	Hyp	Ref	Expression
1		sp 1747	. 2 ⊢ (∀xφ → φ)
2		sps.1	. 2 ⊢ (φ → ψ)
3	1, 2	syl 15	1 ⊢ (∀xφ → ψ)

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  19.2g  1757  ax10lem4  1941  ax10lem6  1943  ax10o  1952  cbv1h  1978  equveli  1988  ax11v2  1992  drsb1  2022  dfsb2  2055  sbequi  2059  drsb2  2061  sbn  2062  sbi1  2063  nfsb4t  2080  sbco2  2086  sbcom  2089  sbcom2  2114  sbal1  2126  eujustALT  2207  mopick  2266  eupickbi  2270  ralcom2  2776  ceqsalg  2884  reu6  3026  sbcal  3094  csbie2t  3181  reldisj  3595  dfnfc2  3910  mosubopt  4613  ssopab2  4713  dfid3  4769  fununi  5161  fv3  5342  fnoprabg  5586  fundmen  6044