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 2190
Description: Inference form of 19.21 2209 and also deduction form of sp 2184. (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 2184 . 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 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-12 2179
This theorem depends on definitions:  df-bi 210  df-ex 1787
This theorem is referenced by:  19.21bbi  2191  axc7e  2320  eleq2w2  2734  eqeq1dALT  2741  eleq2dALT  2819  nfeqd  2909  sselOLD  3871  poclOLD  5450  funmo  6355  funun  6385  fununi  6414  findcard  8762  findcard2  8763  ssfi  8772  findcard2OLD  8834  axpowndlem4  10100  axregndlem2  10103  axinfnd  10106  prcdnq  10493  dfrtrcl2  14511  relexpindlem  14512  bnj1379  32381  bnj1052  32526  bnj1118  32535  bnj1154  32550  bnj1280  32571  dftrcl3  40874  dfrtrcl3  40887  vk15.4j  41686  hbimpg  41712
  Copyright terms: Public domain W3C validator