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 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  2226  axc7e  2348  eleq2w2  2756  eqeq1dALT  2763  eleq2dALT  2847  nfeqd  2932  funun  6579  fununi  6608  findcard  9158  findcard2  9159  ssfi  9167  ttrclselem2  9705  axpowndlem4  10609  axregndlem2  10612  axinfnd  10615  prcdnq  11002  dfrtrcl2  15135  relexpindlem  15136  bnj1379  35339  bnj1052  35484  bnj1118  35493  bnj1154  35508  bnj1280  35529  gblacfnacd  35699  onvf1odlem4  35703  mh-setind  37155  mh-setindnd  37156  dftrcl3  44560  dfrtrcl3  44573  vk15.4j  45351  hbimpg  45377  pgindnf  50642