Theorem 19.21bi 1922

Description: Inference form of 19.21 1962 and also deduction form of sp 1912. (Contributed by NM, 26-May-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		sp 1912	. 2 |- ( A. x ps -> ps )
3	1, 2	syl 17	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   A.wal 1435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-12 1907

This theorem depends on definitions:  df-bi 188  df-ex 1660

This theorem is referenced by:  19.21bbi  1923  2ax6e  2246  eqeq1dALT  2432  eqeq1OLD  2434  eleq2dALT  2500  eleq2OLD  2504  r19.21biOLD  2802  elrab3t  3234  ssel  3464  pocl  4782  funmo  5617  funun  5643  fununi  5667  findcard  7816  findcard2  7817  axpowndlem4  9023  axregndlem2  9026  axinfnd  9030  prcdnq  9417  dfrtrcl2  13104  relexpindlem  13105  bnj1379  29430  bnj1052  29572  bnj1118  29581  bnj1154  29596  bnj1280  29617  dftrcl3  35951  dfrtrcl3  35964  vk15.4j  36522  hbimpg  36558