Theorem 19.21bi 2190

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778

This theorem is referenced by:  19.21bbi  2191  axc7e  2322  eleq2w2  2736  eqeq1dALT  2743  eleq2dALT  2831  nfeqd  2919  poclOLD  5616  funmoOLD  6594  funun  6624  fununi  6653  findcard  9229  findcard2  9230  ssfi  9240  ttrclselem2  9795  axpowndlem4  10669  axregndlem2  10672  axinfnd  10675  prcdnq  11062  dfrtrcl2  15111  relexpindlem  15112  bnj1379  34806  bnj1052  34951  bnj1118  34960  bnj1154  34975  bnj1280  34996  gblacfnacd  35075  dftrcl3  43682  dfrtrcl3  43695  vk15.4j  44499  hbimpg  44525  pgindnf  48808