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 2188
Description: Inference form of 19.21 2207 and also deduction form of sp 2182. (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 2182 . 2 (∀𝑥𝜓𝜓)
31, 2syl 17 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177
This theorem depends on definitions:  df-bi 209  df-ex 1781
This theorem is referenced by:  19.21bbi  2189  axc7e  2337  eqeq1dALT  2823  eleq2dALT  2897  ssel  3940  pocl  5457  funmo  6347  funun  6376  fununi  6405  findcard  8735  findcard2  8736  axpowndlem4  10000  axregndlem2  10003  axinfnd  10006  prcdnq  10393  dfrtrcl2  14401  relexpindlem  14402  bnj1379  32110  bnj1052  32255  bnj1118  32264  bnj1154  32279  bnj1280  32300  dftrcl3  40200  dfrtrcl3  40213  vk15.4j  41017  hbimpg  41043
  Copyright terms: Public domain W3C validator