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  funmoOLD  6532  funun  6562  fununi  6591  findcard  9127  findcard2  9128  ssfi  9137  ttrclselem2  9679  axpowndlem4  10553  axregndlem2  10556  axinfnd  10559  prcdnq  10946  dfrtrcl2  15028  relexpindlem  15029  bnj1379  34820  bnj1052  34965  bnj1118  34974  bnj1154  34989  bnj1280  35010  gblacfnacd  35089  onvf1odlem4  35093  dftrcl3  43709  dfrtrcl3  43722  vk15.4j  44518  hbimpg  44544  pgindnf  49705