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  4341  copsex2t  4387  pocl  4450  ordsucim  4649  peano2  4744  funmo  5395  funun  5425  fununi  5452  imain  5466  tfrlem3-2d  6588  tfr1onlemaccex  6624  tfri1dALT  6627  tfrcllemaccex  6637  findcard  7198  findcard2  7199  findcard2s  7200  exmidpw  7221  exmidpweq  7222  nninfctlemfo  12841