Theorem 19.21bi 2184

Description: Inference form of 19.21 2203 and also deduction form of sp 2178. (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 2178	. 2 ⊢ (∀𝑥𝜓 → 𝜓)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  19.21bbi  2185  axc7e  2316  eleq2w2  2734  eqeq1dALT  2741  eleq2dALT  2825  nfeqd  2916  sselOLD  3911  poclOLD  5502  funmo  6434  funun  6464  fununi  6493  findcard  8908  findcard2  8909  ssfi  8918  findcard2OLD  8986  axpowndlem4  10287  axregndlem2  10290  axinfnd  10293  prcdnq  10680  dfrtrcl2  14701  relexpindlem  14702  bnj1379  32710  bnj1052  32855  bnj1118  32864  bnj1154  32879  bnj1280  32900  ttrclselem2  33712  dftrcl3  41217  dfrtrcl3  41230  vk15.4j  42037  hbimpg  42063