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 2180
Description: Inference form of 19.21 2198 and also deduction form of sp 2174. (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 2174 . 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 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-12 2169
This theorem depends on definitions:  df-bi 206  df-ex 1780
This theorem is referenced by:  19.21bbi  2181  axc7e  2309  eleq2w2  2726  eqeq1dALT  2733  eleq2dALT  2818  nfeqd  2911  sselOLD  3975  poclOLD  5595  funmoOLD  6563  funun  6593  fununi  6622  findcard  9165  findcard2  9166  ssfi  9175  findcard2OLD  9286  ttrclselem2  9723  axpowndlem4  10597  axregndlem2  10600  axinfnd  10603  prcdnq  10990  dfrtrcl2  15013  relexpindlem  15014  bnj1379  34139  bnj1052  34284  bnj1118  34293  bnj1154  34308  bnj1280  34329  dftrcl3  42773  dfrtrcl3  42786  vk15.4j  43591  hbimpg  43617  pgindnf  47848
  Copyright terms: Public domain W3C validator