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  2775  ceqsalg  2883  reu6  3025  sbcal  3093  csbie2t  3180  reldisj  3594  dfnfc2  3909  mosubopt  4612  ssopab2  4712  dfid3  4768  fununi  5160  fv3  5341  fnoprabg  5585  fundmen  6043