Theorem 19.21bi 1572

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

This theorem is referenced by:  19.21bbi  1573  ax11e  1810  eqeq1  2203  eleq2  2260  r19.21bi  2585  elrab3t  2919  ssel  3178  exmidsssn  4236  copsex2t  4279  pocl  4339  ordsucim  4537  peano2  4632  funmo  5274  funun  5303  fununi  5327  imain  5341  tfrlem3-2d  6379  tfr1onlemaccex  6415  tfri1dALT  6418  tfrcllemaccex  6428  findcard  6958  findcard2  6959  findcard2s  6960  exmidpw  6978  exmidpweq  6979  nninfctlemfo  12232