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 2178
Description: Inference form of 19.21 2197 and also deduction form of sp 2172. (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 2172 . 2 (∀𝑥𝜓𝜓)
31, 2syl 17 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  19.21bbi  2179  axc7e  2328  eqeq1dALT  2821  eleq2dALT  2896  ssel  3958  pocl  5474  funmo  6364  funun  6393  fununi  6422  findcard  8745  findcard2  8746  axpowndlem4  10010  axregndlem2  10013  axinfnd  10016  prcdnq  10403  dfrtrcl2  14409  relexpindlem  14410  bnj1379  32001  bnj1052  32144  bnj1118  32153  bnj1154  32168  bnj1280  32189  dftrcl3  39943  dfrtrcl3  39956  vk15.4j  40739  hbimpg  40765
  Copyright terms: Public domain W3C validator