Theorem 19.21bi 1611

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

This proof depends on syntax axioms:   -> wi 4   A.wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1563

This theorem is used by:  19.21bbi  1612  ax11e  1849  eqeq1  2245  eleq2  2302  r19.21bi  2638  elrab3t  2981  ssel  3242  exmidsssn  4339  copsex2t  4385  pocl  4448  ordsucim  4647  peano2  4742  funmo  5392  funun  5422  fununi  5449  imain  5463  tfrlem3-2d  6583  tfr1onlemaccex  6619  tfri1dALT  6622  tfrcllemaccex  6632  findcard  7192  findcard2  7193  findcard2s  7194  exmidpw  7215  exmidpweq  7216  nninfctlemfo  12817