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

Theorem biimp3ar 1285
Description: Infer implication from a logical equivalence. Similar to biimpar 473. (Contributed by NM, 2-Jan-2009.)
Hypothesis
Ref Expression
biimp3a.1  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
Assertion
Ref Expression
biimp3ar  |-  ( (
ph  /\  ps  /\  th )  ->  ch )

Proof of Theorem biimp3ar
StepHypRef Expression
1 biimp3a.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
21exbiri 607 . 2  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
323imp 1148 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    /\ w3a 937
This theorem is referenced by:  rmoi  3252  brelrng  5102  div2sub  9844  abssubge0  12136  qredeu  13112  abvne0  15920  basgen2  17059  fcfval  18070  nmne0  18670  ovolfsf  19373  lgssq  21124  lgssq2  21125  nv1  22170  adjeq  23443  colinearalg  25854  areacirc  26311  fvopabf4g  26436  exidreslem  26566  ssfz12  28127  ssfzo12  28153  iunconlem2  29121  hgmapvvlem3  32800
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator