Theorem 19.21bi 1538

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

Syntax hints:   -> wi 4   A.wal 1330

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

This theorem is referenced by:  19.21bbi  1539  ax11e  1769  eqeq1  2147  eleq2  2204  r19.21bi  2523  elrab3t  2843  ssel  3096  exmidsssn  4133  copsex2t  4175  pocl  4233  ordsucim  4424  peano2  4517  funmo  5146  funun  5175  fununi  5199  imain  5213  tfrlem3-2d  6217  tfr1onlemaccex  6253  tfri1dALT  6256  tfrcllemaccex  6266  findcard  6790  findcard2  6791  findcard2s  6792  exmidpw  6810