Theorem 19.21bi 1818

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 1808	. 2 |- ( A. x ps -> ps )
3	1, 2	syl 16	1 |- ( ph -> ps )

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:  19.21bbi  1908  equveliOLD  2062  2ax6e  2180  eqeq1dALT  2470  eqeq1OLD  2472  eleq2dALT  2538  eleq2OLD  2542  r19.21biOLD  2834  elrab3t  3260  ssel  3498  pocl  4807  funmo  5604  funun  5630  fununi  5654  findcard  7759  findcard2  7760  axpowndlem2OLD  8974  axpowndlem4  8977  axregndlem2  8980  axinfnd  8984  prcdnq  9371  relexpindlem  28565  dfrtrcl2  28574  vk15.4j  32395  hbimpg  32425  bnj1379  32986  bnj1052  33128  bnj1118  33137  bnj1154  33152  bnj1280  33173