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

Theorem exbiri 622
Description: Inference form of exbir 31509. This proof is exbiriVD 31945 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.)
Hypothesis
Ref Expression
exbiri.1  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
Assertion
Ref Expression
exbiri  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )

Proof of Theorem exbiri
StepHypRef Expression
1 exbiri.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
21biimpar 485 . 2  |-  ( ( ( ph  /\  ps )  /\  th )  ->  ch )
32exp31 604 1  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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
This theorem is referenced by:  biimp3ar  1320  eqrdavOLD  2453  tfrlem9  6957  sbthlem1  7534  addcanpr  9330  axpre-sup  9451  lbreu  10395  zmax  11065  uzsubsubfz  11592  elfzodifsumelfzo  11725  swrdccatin12lem3  12503  cshwidxmod  12562  ucnima  19998  usgraidx2vlem2  23489  mdslmd1lem1  25908  mdslmd1lem2  25909  dfon2  27772  cgrextend  28206  brsegle  28306  brabg2  28780  ralxfrd2  30308  elfzom1elp1fzo  30389  wwlkextwrd  30531  numclwlk1lem2f1  30858
  Copyright terms: Public domain W3C validator