MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.21bi Structured version   Visualization version   GIF version

Theorem 19.21bi 2182
Description: Inference form of 19.21 2200 and also deduction form of sp 2176. (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
19.21bi.1 (𝜑 → ∀𝑥𝜓)
Assertion
Ref Expression
19.21bi (𝜑𝜓)

Proof of Theorem 19.21bi
StepHypRef Expression
1 19.21bi.1 . 2 (𝜑 → ∀𝑥𝜓)
2 sp 2176 . 2 (∀𝑥𝜓𝜓)
31, 2syl 17 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1537
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 1913  ax-6 1971  ax-7 2011  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  19.21bbi  2183  axc7e  2312  eleq2w2  2734  eqeq1dALT  2741  eleq2dALT  2825  nfeqd  2917  sselOLD  3915  poclOLD  5511  funmo  6450  funun  6480  fununi  6509  findcard  8946  findcard2  8947  ssfi  8956  findcard2OLD  9056  ttrclselem2  9484  axpowndlem4  10356  axregndlem2  10359  axinfnd  10362  prcdnq  10749  dfrtrcl2  14773  relexpindlem  14774  bnj1379  32810  bnj1052  32955  bnj1118  32964  bnj1154  32979  bnj1280  33000  dftrcl3  41328  dfrtrcl3  41341  vk15.4j  42148  hbimpg  42174
  Copyright terms: Public domain W3C validator