Theorem 19.21bi 1490

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

Syntax hints:   -> wi 4   A.wal 1282

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

This theorem is referenced by:  19.21bbi  1491  ax11e  1717  eqeq1  2087  eleq2  2142  r19.21bi  2449  elrab3t  2748  ssel  2993  copsex2t  4000  pocl  4058  ordsucim  4244  peano2  4336  funmo  4937  funun  4964  fununi  4987  imain  5001  tfrlem3-2d  5951  findcard  6372  findcard2  6373  findcard2s  6374