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  2319  eleq2w2  2732  eqeq1dALT  2739  eleq2dALT  2822  nfeqd  2910  funmoOLD  6557  funun  6587  fununi  6616  findcard  9182  findcard2  9183  ssfi  9192  ttrclselem2  9745  axpowndlem4  10619  axregndlem2  10622  axinfnd  10625  prcdnq  11012  dfrtrcl2  15086  relexpindlem  15087  bnj1379  34866  bnj1052  35011  bnj1118  35020  bnj1154  35035  bnj1280  35056  gblacfnacd  35135  dftrcl3  43711  dfrtrcl3  43724  vk15.4j  44520  hbimpg  44546  pgindnf  49547