Theorem 19.21bi 2182

Description: Inference form of 19.21 2200 and also deduction form of sp 2176. (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 2176	. 2 ⊢ (∀𝑥𝜓 → 𝜓)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  19.21bbi  2183  axc7e  2312  eleq2w2  2734  eqeq1dALT  2741  eleq2dALT  2825  nfeqd  2917  sselOLD  3915  poclOLD  5511  funmo  6450  funun  6480  fununi  6509  findcard  8946  findcard2  8947  ssfi  8956  findcard2OLD  9056  ttrclselem2  9484  axpowndlem4  10356  axregndlem2  10359  axinfnd  10362  prcdnq  10749  dfrtrcl2  14773  relexpindlem  14774  bnj1379  32810  bnj1052  32955  bnj1118  32964  bnj1154  32979  bnj1280  33000  dftrcl3  41328  dfrtrcl3  41341  vk15.4j  42148  hbimpg  42174