Theorem 19.21bi 2186

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

Syntax hints:   → wi 4  ∀wal 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-ex 1782

This theorem is referenced by:  19.21bbi  2187  axc7e  2326  eqeq1dALT  2801  eleq2dALT  2876  nfeqd  2965  sselOLD  3909  pocl  5445  funmo  6340  funun  6370  fununi  6399  findcard  8741  findcard2  8742  axpowndlem4  10011  axregndlem2  10014  axinfnd  10017  prcdnq  10404  dfrtrcl2  14413  relexpindlem  14414  bnj1379  32212  bnj1052  32357  bnj1118  32366  bnj1154  32381  bnj1280  32402  dftrcl3  40421  dfrtrcl3  40434  vk15.4j  41234  hbimpg  41260