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  6546  fununi  6575  findcard  9104  findcard2  9105  ssfi  9114  ttrclselem2  9655  axpowndlem4  10529  axregndlem2  10532  axinfnd  10535  prcdnq  10922  dfrtrcl2  15004  relexpindlem  15005  bnj1379  34793  bnj1052  34938  bnj1118  34947  bnj1154  34962  bnj1280  34983  gblacfnacd  35062  onvf1odlem4  35066  dftrcl3  43682  dfrtrcl3  43695  vk15.4j  44491  hbimpg  44517  pgindnf  49678