Theorem 19.21bi 1607

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

Syntax hints:   -> wi 4   A.wal 1396

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

This theorem is referenced by:  19.21bbi  1608  ax11e  1845  eqeq1  2241  eleq2  2298  r19.21bi  2632  elrab3t  2975  ssel  3236  exmidsssn  4320  copsex2t  4366  pocl  4429  ordsucim  4627  peano2  4722  funmo  5372  funun  5402  fununi  5429  imain  5443  tfrlem3-2d  6556  tfr1onlemaccex  6592  tfri1dALT  6595  tfrcllemaccex  6605  findcard  7158  findcard2  7159  findcard2s  7160  exmidpw  7181  exmidpweq  7182  nninfctlemfo  12761