Theorem 19.21bi 2192

Description: Inference form of 19.21 2210 and also deduction form of sp 2186. (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 2186	. 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 2180

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

This theorem is referenced by:  19.21bbi  2193  axc7e  2319  eleq2w2  2727  eqeq1dALT  2734  eleq2dALT  2818  nfeqd  2905  funun  6522  fununi  6551  findcard  9068  findcard2  9069  ssfi  9077  ttrclselem2  9611  axpowndlem4  10486  axregndlem2  10489  axinfnd  10492  prcdnq  10879  dfrtrcl2  14964  relexpindlem  14965  bnj1379  34834  bnj1052  34979  bnj1118  34988  bnj1154  35003  bnj1280  35024  gblacfnacd  35138  onvf1odlem4  35142  dftrcl3  43753  dfrtrcl3  43766  vk15.4j  44561  hbimpg  44587  pgindnf  49748