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  2916  ssel  3174  exmidsssn  4232  copsex2t  4275  pocl  4335  ordsucim  4533  peano2  4628  funmo  5270  funun  5299  fununi  5323  imain  5337  tfrlem3-2d  6367  tfr1onlemaccex  6403  tfri1dALT  6406  tfrcllemaccex  6416  findcard  6946  findcard2  6947  findcard2s  6948  exmidpw  6966  exmidpweq  6967  nninfctlemfo  12180