Theorem 19.21bi 1569

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 1521	. 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 1521

This theorem is referenced by:  19.21bbi  1570  ax11e  1807  eqeq1  2200  eleq2  2257  r19.21bi  2582  elrab3t  2915  ssel  3173  exmidsssn  4231  copsex2t  4274  pocl  4334  ordsucim  4532  peano2  4627  funmo  5269  funun  5298  fununi  5322  imain  5336  tfrlem3-2d  6365  tfr1onlemaccex  6401  tfri1dALT  6404  tfrcllemaccex  6414  findcard  6944  findcard2  6945  findcard2s  6946  exmidpw  6964  exmidpweq  6965  nninfctlemfo  12177