Theorem 19.21bi 1809

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-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 1799	. 2 |- ( A. x ps -> ps )
3	1, 2	syl 16	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   A.wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797

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

This theorem is referenced by:  19.21bbi  1891  equveliOLD  2044  2sb6rflem2  2163  eqeq1  2447  eleq2  2502  r19.21bi  2812  elrab3t  3113  ssel  3347  pocl  4644  funmo  5431  funun  5457  fununi  5481  findcard  7547  findcard2  7548  axpowndlem2OLD  8759  axpowndlem4  8762  axregndlem2  8765  axinfnd  8769  prcdnq  9158  relexpindlem  27270  dfrtrcl2  27279  vk15.4j  31066  hbimpg  31096  bnj1379  31658  bnj1052  31800  bnj1118  31809  bnj1154  31824  bnj1280  31845