Theorem 19.21bi 1611

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		ax-4 1563	. 2 |- ( A. x ps -> ps )
3	1, 2	syl 14	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   A.wal 1400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1563

This theorem is referenced by:  19.21bbi  1612  ax11e  1849  eqeq1  2245  eleq2  2302  r19.21bi  2638  elrab3t  2981  ssel  3242  exmidsssn  4334  copsex2t  4380  pocl  4443  ordsucim  4642  peano2  4737  funmo  5387  funun  5417  fununi  5444  imain  5458  tfrlem3-2d  6573  tfr1onlemaccex  6609  tfri1dALT  6612  tfrcllemaccex  6622  findcard  7182  findcard2  7183  findcard2s  7184  exmidpw  7205  exmidpweq  7206  nninfctlemfo  12795