Theorem 19.21bi 1958

Description: Inference form of 19.21 1998 and also deduction form of sp 1948. (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 1948	. 2 |- ( A. x ps -> ps )
3	1, 2	syl 17	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   A.wal 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-12 1944

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675

This theorem is referenced by:  19.21bbi  1959  2ax6e  2290  eqeq1dALT  2465  eleq2dALT  2527  r19.21biOLD  2770  elrab3t  3207  ssel  3438  pocl  4781  funmo  5617  funun  5643  fununi  5671  findcard  7836  findcard2  7837  axpowndlem4  9051  axregndlem2  9054  axinfnd  9057  prcdnq  9444  dfrtrcl2  13174  relexpindlem  13175  bnj1379  29691  bnj1052  29833  bnj1118  29842  bnj1154  29857  bnj1280  29878  dftrcl3  36357  dfrtrcl3  36370  vk15.4j  36929  hbimpg  36965