Theorem 19.21bi 1558

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

Syntax hints:   -> wi 4   A.wal 1351

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

This theorem is referenced by:  19.21bbi  1559  ax11e  1796  eqeq1  2184  eleq2  2241  r19.21bi  2565  elrab3t  2894  ssel  3151  exmidsssn  4204  copsex2t  4247  pocl  4305  ordsucim  4501  peano2  4596  funmo  5233  funun  5262  fununi  5286  imain  5300  tfrlem3-2d  6315  tfr1onlemaccex  6351  tfri1dALT  6354  tfrcllemaccex  6364  findcard  6890  findcard2  6891  findcard2s  6892  exmidpw  6910  exmidpweq  6911