Theorem spsd 2057

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 2053	. 2 |- ( A. x ps -> ps )
2		spsd.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 34	1 |- ( ph -> ( A. x ps -> ch ) )

Syntax hints:   -> wi 4   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  axc11v  2138  axc11rv  2139  axc11rvOLD  2140  axc11nlemOLD  2160  axc11nlemALT  2306  equvel  2347  nfsb4t  2389  mo2v  2477  moexex  2541  2eu6  2558  zorn2lem4  9321  zorn2lem5  9322  axpowndlem3  9421  axacndlem5  9433  axc11n11r  32673  wl-equsal1i  33329  axc5c4c711  38602