Theorem 19.21bi 2229

Description: Inference form of 19.21 2247 and also deduction form of sp 2223. (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 2223	. 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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  19.21bbi  2230  axc7e  2352  eleq2w2  2759  eqeq1dALT  2766  eleq2dALT  2851  nfeqd  2936  funun  6614  fununi  6645  findcard  9217  findcard2  9218  ssfi  9226  ttrclselem2  9764  axpowndlem4  10724  axregndlem2  10727  axinfnd  10730  prcdnq  11117  dfrtrcl2  15258  relexpindlem  15259  bnj1379  35571  bnj1052  35716  bnj1118  35725  bnj1154  35740  bnj1280  35761  gblacfnacd  36070  onvf1odlem4  36075  srepdf  36128  smrepsrep  36129  mh-setind  37539  mh-setindnd  37540  dftrcl3  44981  dfrtrcl3  44994  vk15.4j  45771  hbimpg  45797  pgindnf  51215