Theorem 19.21bi 1450

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

Syntax hints:   -> wi 4   A.wal 1241

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

This theorem is referenced by:  19.21bbi  1451  ax11e  1677  eqeq1  2046  eleq2  2101  r19.21bi  2407  elrab3t  2697  ssel  2939  copsex2t  3982  pocl  4040  ordsucim  4226  peano2  4318  funmo  4917  funun  4944  fununi  4967  imain  4981  tfrlem3-2d  5928  findcard  6345  findcard2  6346  findcard2s  6347