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

Theorem exbiri 626
Description: Inference form of exbir 36804. This proof is exbiriVD 37224 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 487 . 2  |-  ( ( ( ph  /\  ps )  /\  th )  ->  ch )
32exp31 607 1  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  biimp3ar  1365  eqrdavOLD  2421  tfrlem9  7115  sbthlem1  7692  addcanpr  9479  axpre-sup  9601  lbreu  10564  zmax  11269  uzsubsubfz  11829  elfzodifsumelfzo  11987  swrdccatin12lem3  12849  cshwidxmod  12908  prmgaplem6  15026  ucnima  21295  usgraidx2vlem2  25118  wwlkextwrd  25455  numclwlk1lem2f1  25821  mdslmd1lem1  27977  mdslmd1lem2  27978  dfon2  30446  cgrextend  30781  brsegle  30881  finxpsuclem  31754  poimirlem18  31923  poimirlem21  31926  brabg2  32007  iccelpart  38618  ralxfrd2  38873  usgridx2vlem2  39108
  Copyright terms: Public domain W3C validator