Theorem 19.21bi 1546

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

Syntax hints:   -> wi 4   A.wal 1341

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

This theorem is referenced by:  19.21bbi  1547  ax11e  1784  eqeq1  2172  eleq2  2230  r19.21bi  2554  elrab3t  2881  ssel  3136  exmidsssn  4181  copsex2t  4223  pocl  4281  ordsucim  4477  peano2  4572  funmo  5203  funun  5232  fununi  5256  imain  5270  tfrlem3-2d  6280  tfr1onlemaccex  6316  tfri1dALT  6319  tfrcllemaccex  6329  findcard  6854  findcard2  6855  findcard2s  6856  exmidpw  6874  exmidpweq  6875