MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exbiri Unicode version

Theorem exbiri 622
Description: Inference form of exbir 31997. This proof is exbiriVD 32433 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.)
Hypothesis
Ref Expression
exbiri.1
Assertion
Ref Expression
exbiri

Proof of Theorem exbiri
StepHypRef Expression
1 exbiri.1 . . 3
21biimpar 485 . 2
32exp31 604 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  biimp3ar  1320  eqrdavOLD  2453  tfrlem9  6978  sbthlem1  7555  addcanpr  9352  axpre-sup  9473  lbreu  10417  zmax  11089  uzsubsubfz  11616  elfzodifsumelfzo  11749  swrdccatin12lem3  12539  cshwidxmod  12598  ucnima  20255  usgraidx2vlem2  23779  mdslmd1lem1  26198  mdslmd1lem2  26199  dfon2  28061  cgrextend  28495  brsegle  28595  brabg2  29069  ralxfrd2  31014  elfzom1elp1fzo  31095  wwlkextwrd  31237  numclwlk1lem2f1  31564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator