Theorem 19.21bi 1551

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

Syntax hints:   -> wi 4   A.wal 1346

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

This theorem is referenced by:  19.21bbi  1552  ax11e  1789  eqeq1  2177  eleq2  2234  r19.21bi  2558  elrab3t  2885  ssel  3141  exmidsssn  4186  copsex2t  4228  pocl  4286  ordsucim  4482  peano2  4577  funmo  5211  funun  5240  fununi  5264  imain  5278  tfrlem3-2d  6289  tfr1onlemaccex  6325  tfri1dALT  6328  tfrcllemaccex  6338  findcard  6864  findcard2  6865  findcard2s  6866  exmidpw  6884  exmidpweq  6885