Theorem 19.21bi 2197

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

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  19.21bbi  2198  axc7e  2324  eleq2w2  2733  eqeq1dALT  2740  eleq2dALT  2824  nfeqd  2910  funun  6538  fununi  6567  findcard  9091  findcard2  9092  ssfi  9100  ttrclselem2  9638  axpowndlem4  10514  axregndlem2  10517  axinfnd  10520  prcdnq  10907  dfrtrcl2  15015  relexpindlem  15016  bnj1379  34988  bnj1052  35133  bnj1118  35142  bnj1154  35157  bnj1280  35178  gblacfnacd  35300  onvf1odlem4  35304  mh-setind  36734  mh-setindnd  36735  dftrcl3  44165  dfrtrcl3  44178  vk15.4j  44973  hbimpg  44999  pgindnf  50203