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 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
StepHypRef Expression
1 19.21bi.1 . 2 (𝜑 → ∀𝑥𝜓)
2 sp 2177 . 2 (∀𝑥𝜓𝜓)
31, 2syl 17 1 (𝜑𝜓)
Colors of variables: wff setvar class
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  3974  poclOLD  5592  funmoOLD  6556  funun  6586  fununi  6615  findcard  9151  findcard2  9152  ssfi  9161  findcard2OLD  9272  ttrclselem2  9708  axpowndlem4  10582  axregndlem2  10585  axinfnd  10588  prcdnq  10975  dfrtrcl2  14996  relexpindlem  14997  bnj1379  33772  bnj1052  33917  bnj1118  33926  bnj1154  33941  bnj1280  33962  dftrcl3  42342  dfrtrcl3  42355  vk15.4j  43160  hbimpg  43186  pgindnf  47601
  Copyright terms: Public domain W3C validator