Theorem 19.21bi 2183

Description: Inference form of 19.21 2201 and also deduction form of sp 2177. (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 2177	. 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  19.21bbi  2184  axc7e  2312  eleq2w2  2729  eqeq1dALT  2736  eleq2dALT  2821  nfeqd  2914  sselOLD  3977  poclOLD  5597  funmoOLD  6565  funun  6595  fununi  6624  findcard  9163  findcard2  9164  ssfi  9173  findcard2OLD  9284  ttrclselem2  9721  axpowndlem4  10595  axregndlem2  10598  axinfnd  10601  prcdnq  10988  dfrtrcl2  15009  relexpindlem  15010  bnj1379  33841  bnj1052  33986  bnj1118  33995  bnj1154  34010  bnj1280  34031  dftrcl3  42471  dfrtrcl3  42484  vk15.4j  43289  hbimpg  43315  pgindnf  47761