Theorem 19.21bi 2196

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

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

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

This theorem is referenced by:  19.21bbi  2197  axc7e  2323  eleq2w2  2732  eqeq1dALT  2739  eleq2dALT  2823  nfeqd  2909  funun  6538  fununi  6567  findcard  9088  findcard2  9089  ssfi  9097  ttrclselem2  9635  axpowndlem4  10511  axregndlem2  10514  axinfnd  10517  prcdnq  10904  dfrtrcl2  14985  relexpindlem  14986  bnj1379  34986  bnj1052  35131  bnj1118  35140  bnj1154  35155  bnj1280  35176  gblacfnacd  35296  onvf1odlem4  35300  mh-setind  36666  mh-setindnd  36667  dftrcl3  43961  dfrtrcl3  43974  vk15.4j  44769  hbimpg  44795  pgindnf  49961