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 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

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

This theorem is referenced by:  19.21bbi  2191  axc7e  2317  eleq2w2  2726  eqeq1dALT  2733  eleq2dALT  2816  nfeqd  2903  funmoOLD  6535  funun  6565  fununi  6594  findcard  9133  findcard2  9134  ssfi  9143  ttrclselem2  9686  axpowndlem4  10560  axregndlem2  10563  axinfnd  10566  prcdnq  10953  dfrtrcl2  15035  relexpindlem  15036  bnj1379  34827  bnj1052  34972  bnj1118  34981  bnj1154  34996  bnj1280  35017  gblacfnacd  35096  onvf1odlem4  35100  dftrcl3  43716  dfrtrcl3  43729  vk15.4j  44525  hbimpg  44551  pgindnf  49709