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 32591. This proof is exbiriVD 33027 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  1329  eqrdavOLD  2466  tfrlem9  7064  sbthlem1  7637  addcanpr  9434  axpre-sup  9556  lbreu  10503  zmax  11189  uzsubsubfz  11717  elfzodifsumelfzo  11860  swrdccatin12lem3  12690  cshwidxmod  12749  ucnima  20629  usgraidx2vlem2  24183  wwlkextwrd  24519  numclwlk1lem2f1  24886  mdslmd1lem1  27035  mdslmd1lem2  27036  dfon2  29119  cgrextend  29553  brsegle  29653  brabg2  30101  ralxfrd2  32061
  Copyright terms: Public domain W3C validator