Theorem 19.21bi 2225

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

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

This theorem is used by:  19.21bbi  2226  axc7e  2348  eleq2w2  2756  eqeq1dALT  2763  eleq2dALT  2847  nfeqd  2932  funun  6589  fununi  6618  findcard  9184  findcard2  9185  ssfi  9193  ttrclselem2  9732  axpowndlem4  10690  axregndlem2  10693  axinfnd  10696  prcdnq  11083  dfrtrcl2  15222  relexpindlem  15223  bnj1379  35508  bnj1052  35653  bnj1118  35662  bnj1154  35677  bnj1280  35698  gblacfnacd  35950  onvf1odlem4  35955  srepdf  36008  smrepsrep  36009  mh-setind  37418  mh-setindnd  37419  dftrcl3  44827  dfrtrcl3  44840  vk15.4j  45618  hbimpg  45644  pgindnf  50991