Theorem exbiri 622

Description: Inference form of exbir 33219. This proof is exbiriVD 33654 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

Step	Hyp	Ref	Expression
1		exbiri.1	. . 3
2	1	biimpar 485	. 2
3	2	exp31 604	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  biimp3ar  1329  eqrdavOLD  2456  tfrlem9  7073  sbthlem1  7647  addcanpr  9445  axpre-sup  9567  lbreu  10518  zmax  11208  uzsubsubfz  11736  elfzodifsumelfzo  11882  swrdccatin12lem3  12715  cshwidxmod  12774  ucnima  20784  usgraidx2vlem2  24392  wwlkextwrd  24728  numclwlk1lem2f1  25094  mdslmd1lem1  27244  mdslmd1lem2  27245  dfon2  29224  cgrextend  29658  brsegle  29758  brabg2  30206  ralxfrd2  32303

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