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 1539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-ex 1782
This theorem is referenced by:  19.21bbi  2183  axc7e  2311  eleq2w2  2728  eqeq1dALT  2735  eleq2dALT  2820  nfeqd  2913  sselOLD  3976  poclOLD  5596  funmoOLD  6564  funun  6594  fununi  6623  findcard  9162  findcard2  9163  ssfi  9172  findcard2OLD  9283  ttrclselem2  9720  axpowndlem4  10594  axregndlem2  10597  axinfnd  10600  prcdnq  10987  dfrtrcl2  15008  relexpindlem  15009  bnj1379  33836  bnj1052  33981  bnj1118  33990  bnj1154  34005  bnj1280  34026  dftrcl3  42461  dfrtrcl3  42474  vk15.4j  43279  hbimpg  43305  pgindnf  47751
  Copyright terms: Public domain W3C validator