Theorem 19.21bi 2231

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

Syntax hints:   → wi 4  ∀wal 1565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

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

This theorem is referenced by:  19.21bbi  2232  axc7e  2357  eleq2w2  2765  eqeq1dALT  2772  eleq2dALT  2856  nfeqd  2941  funun  6583  fununi  6612  findcard  9147  findcard2  9148  ssfi  9156  ttrclselem2  9694  axpowndlem4  10584  axregndlem2  10587  axinfnd  10590  prcdnq  10977  dfrtrcl2  15098  relexpindlem  15099  bnj1379  35162  bnj1052  35307  bnj1118  35316  bnj1154  35331  bnj1280  35352  gblacfnacd  35484  onvf1odlem4  35488  mh-setind  36935  mh-setindnd  36936  dftrcl3  44337  dfrtrcl3  44350  vk15.4j  45128  hbimpg  45154  pgindnf  50378