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  4188  copsex2t  4230  pocl  4288  ordsucim  4484  peano2  4579  funmo  5213  funun  5242  fununi  5266  imain  5280  tfrlem3-2d  6291  tfr1onlemaccex  6327  tfri1dALT  6330  tfrcllemaccex  6340  findcard  6866  findcard2  6867  findcard2s  6868  exmidpw  6886  exmidpweq  6887