Theorem 19.21bi 1582

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

Syntax hints:   -> wi 4   A.wal 1371

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

This theorem is referenced by:  19.21bbi  1583  ax11e  1820  eqeq1  2214  eleq2  2271  r19.21bi  2596  elrab3t  2935  ssel  3195  exmidsssn  4262  copsex2t  4307  pocl  4368  ordsucim  4566  peano2  4661  funmo  5305  funun  5334  fununi  5361  imain  5375  tfrlem3-2d  6421  tfr1onlemaccex  6457  tfri1dALT  6460  tfrcllemaccex  6470  findcard  7011  findcard2  7012  findcard2s  7013  exmidpw  7031  exmidpweq  7032  nninfctlemfo  12476