Theorem 19.21bi 2187

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

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

This theorem is referenced by:  19.21bbi  2188  axc7e  2317  eleq2w2  2731  eqeq1dALT  2738  eleq2dALT  2826  nfeqd  2914  funmoOLD  6584  funun  6614  fununi  6643  findcard  9202  findcard2  9203  ssfi  9212  ttrclselem2  9764  axpowndlem4  10638  axregndlem2  10641  axinfnd  10644  prcdnq  11031  dfrtrcl2  15098  relexpindlem  15099  bnj1379  34823  bnj1052  34968  bnj1118  34977  bnj1154  34992  bnj1280  35013  gblacfnacd  35092  dftrcl3  43710  dfrtrcl3  43723  vk15.4j  44526  hbimpg  44552  pgindnf  48947