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

Theorem exbiri 606
Description: Inference form of exbir 1374. This proof is exbiriVD 28903 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 472 . 2  |-  ( ( ( ph  /\  ps )  /\  th )  ->  ch )
32exp31 588 1  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  biimp3ar  1284  eqrdav  2434  tfrlem9  6638  sbthlem1  7209  addcanpr  8915  axpre-sup  9036  lbreu  9950  zmax  10563  ucnima  18303  usgraidx2vlem2  21403  mdslmd1lem1  23820  mdslmd1lem2  23821  dfon2  25411  cgrextend  25934  brsegle  26034  brabg2  26408  ralxfrd2  28059  swrdccatin12lem4  28179  2cshw  28222  2cshwmod  28223
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator