Theorem 19.21bi 2226

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  19.21bbi  2227  axc7e  2349  eleq2w2  2757  eqeq1dALT  2764  eleq2dALT  2848  nfeqd  2933  funun  6584  fununi  6613  findcard  9172  findcard2  9173  ssfi  9181  ttrclselem2  9720  axpowndlem4  10678  axregndlem2  10681  axinfnd  10684  prcdnq  11071  dfrtrcl2  15208  relexpindlem  15209  bnj1379  35453  bnj1052  35598  bnj1118  35607  bnj1154  35622  bnj1280  35643  gblacfnacd  35864  onvf1odlem4  35868  mh-setind  37304  mh-setindnd  37305  dftrcl3  44705  dfrtrcl3  44718  vk15.4j  45496  hbimpg  45522  pgindnf  50778