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

Theorem biimp3ar 1282
Description: Infer implication from a logical equivalence. Similar to biimpar 471. (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 605 . 2  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
323imp 1145 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934
This theorem is referenced by:  rmoi  3080  brelrng  4908  div2sub  9585  abssubge0  11811  qredeu  12786  abvne0  15592  basgen2  16727  fcfval  17728  nmne0  18140  ovolfsf  18831  lgssq  20574  lgssq2  20575  nv1  21242  adjeq  22515  colinearalg  24538  areacirc  24931  cmp2morp  25958  fvopabf4g  26386  exidreslem  26567  hgmapvvlem3  32118
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator