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  4247  copsex2t  4290  pocl  4351  ordsucim  4549  peano2  4644  funmo  5287  funun  5316  fununi  5343  imain  5357  tfrlem3-2d  6400  tfr1onlemaccex  6436  tfri1dALT  6439  tfrcllemaccex  6449  findcard  6987  findcard2  6988  findcard2s  6989  exmidpw  7007  exmidpweq  7008  nninfctlemfo  12394