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  2725  eqeq1dALT  2732  eleq2dALT  2815  nfeqd  2902  funun  6528  fununi  6557  findcard  9077  findcard2  9078  ssfi  9087  ttrclselem2  9622  axpowndlem4  10494  axregndlem2  10497  axinfnd  10500  prcdnq  10887  dfrtrcl2  14969  relexpindlem  14970  bnj1379  34797  bnj1052  34942  bnj1118  34951  bnj1154  34966  bnj1280  34987  gblacfnacd  35075  onvf1odlem4  35079  dftrcl3  43693  dfrtrcl3  43706  vk15.4j  44502  hbimpg  44528  pgindnf  49701