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 32952. This proof is exbiriVD 33387 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  1330  eqrdavOLD  2442  tfrlem9  7056  sbthlem1  7629  addcanpr  9427  axpre-sup  9549  lbreu  10499  zmax  11188  uzsubsubfz  11716  elfzodifsumelfzo  11861  swrdccatin12lem3  12694  cshwidxmod  12753  ucnima  20657  usgraidx2vlem2  24264  wwlkextwrd  24600  numclwlk1lem2f1  24966  mdslmd1lem1  27116  mdslmd1lem2  27117  dfon2  29199  cgrextend  29633  brsegle  29733  brabg2  30181  ralxfrd2  32141
  Copyright terms: Public domain W3C validator