Theorem 19.21bi 2228

Description: Inference form of 19.21 2246 and also deduction form of sp 2222. (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 2222	. 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 2216

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

This theorem is used by:  19.21bbi  2229  axc7e  2353  eleq2w2  2761  eqeq1dALT  2768  eleq2dALT  2852  nfeqd  2937  funun  6586  fununi  6615  findcard  9155  findcard2  9156  ssfi  9164  ttrclselem2  9702  axpowndlem4  10600  axregndlem2  10603  axinfnd  10606  prcdnq  10993  dfrtrcl2  15123  relexpindlem  15124  bnj1379  35283  bnj1052  35428  bnj1118  35437  bnj1154  35452  bnj1280  35473  gblacfnacd  35643  onvf1odlem4  35647  mh-setind  37104  mh-setindnd  37105  dftrcl3  44504  dfrtrcl3  44517  vk15.4j  45295  hbimpg  45321  pgindnf  50551