Theorem 19.21bi 1808

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
19.21bi.1	|- ( ph -> A. x ps )

Assertion

Ref	Expression
19.21bi	|- ( ph -> ps )

Proof of Theorem 19.21bi

Step	Hyp	Ref	Expression
1		19.21bi.1	. 2 |- ( ph -> A. x ps )
2		sp 1798	. 2 |- ( A. x ps -> ps )
3	1, 2	syl 16	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   A.wal 1368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794

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

This theorem is referenced by:  19.21bbi  1898  equveliOLD  2048  2ax6e  2166  eqeq1dALT  2455  eqeq1OLD  2457  eleq2dALT  2523  eleq2OLD  2527  r19.21bi  2914  elrab3t  3217  ssel  3453  pocl  4751  funmo  5537  funun  5563  fununi  5587  findcard  7657  findcard2  7658  axpowndlem2OLD  8869  axpowndlem4  8872  axregndlem2  8875  axinfnd  8879  prcdnq  9268  relexpindlem  27480  dfrtrcl2  27489  vk15.4j  31546  hbimpg  31576  bnj1379  32137  bnj1052  32279  bnj1118  32288  bnj1154  32303  bnj1280  32324