Theorem 19.21bi 1604

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

Syntax hints:   -> wi 4   A.wal 1393

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

This theorem is referenced by:  19.21bbi  1605  ax11e  1842  eqeq1  2236  eleq2  2293  r19.21bi  2618  elrab3t  2958  ssel  3218  exmidsssn  4286  copsex2t  4331  pocl  4394  ordsucim  4592  peano2  4687  funmo  5333  funun  5362  fununi  5389  imain  5403  tfrlem3-2d  6458  tfr1onlemaccex  6494  tfri1dALT  6497  tfrcllemaccex  6507  findcard  7050  findcard2  7051  findcard2s  7052  exmidpw  7070  exmidpweq  7071  nninfctlemfo  12561