Theorem spsd 1816

Description: Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.)

Hypothesis

Ref	Expression
spsd.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
spsd	|- ( ph -> ( A. x ps -> ch ) )

Proof of Theorem spsd

Step	Hyp	Ref	Expression
1		sp 1808	. 2 |- ( A. x ps -> ps )
2		spsd.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 32	1 |- ( ph -> ( A. x ps -> ch ) )

Syntax hints:   -> wi 4   A.wal 1377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803

This theorem depends on definitions:  df-bi 185  df-ex 1597

This theorem is referenced by:  axc11nlem  1885  axc11nlemOLD  2021  equveli  2061  nfsb4t  2103  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  moexex  2371  moexexOLD  2372  2eu6  2393  zorn2lem4  8880  zorn2lem5  8881  axpowndlem3  8976  axpowndlem3OLD  8977  axacndlem5  8990  wl-equsal1i  29849  axc5c4c711  31113  bj-axc11nlemv  33613