Theorem 19.21bi 2225

Description: Inference form of 19.21 2243 and also deduction form of sp 2219. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
19.21bi.1	⊢ (𝜑 → ∀𝑥𝜓)

Assertion

Ref	Expression
19.21bi	⊢ (𝜑 → 𝜓)

Proof of Theorem 19.21bi

Step	Hyp	Ref	Expression
1		19.21bi.1	. 2 ⊢ (𝜑 → ∀𝑥𝜓)
2		sp 2219	. 2 ⊢ (∀𝑥𝜓 → 𝜓)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  19.21bbi  2226  axc7e  2351  eleq2w2  2759  eqeq1dALT  2766  eleq2dALT  2850  nfeqd  2935  funun  6582  fununi  6611  findcard  9144  findcard2  9145  ssfi  9153  ttrclselem2  9691  axpowndlem4  10580  axregndlem2  10583  axinfnd  10586  prcdnq  10973  dfrtrcl2  15095  relexpindlem  15096  bnj1379  35218  bnj1052  35363  bnj1118  35372  bnj1154  35387  bnj1280  35408  gblacfnacd  35586  onvf1odlem4  35590  mh-setind  37047  mh-setindnd  37048  dftrcl3  44446  dfrtrcl3  44459  vk15.4j  45237  hbimpg  45263  pgindnf  50494