Theorem 19.21bi 1581

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

This theorem is referenced by:  19.21bbi  1582  ax11e  1819  eqeq1  2212  eleq2  2269  r19.21bi  2594  elrab3t  2928  ssel  3187  exmidsssn  4246  copsex2t  4289  pocl  4350  ordsucim  4548  peano2  4643  funmo  5286  funun  5315  fununi  5342  imain  5356  tfrlem3-2d  6398  tfr1onlemaccex  6434  tfri1dALT  6437  tfrcllemaccex  6447  findcard  6985  findcard2  6986  findcard2s  6987  exmidpw  7005  exmidpweq  7006  nninfctlemfo  12361