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  3156  brelrng  4990  div2sub  9675  abssubge0  11907  qredeu  12883  abvne0  15691  basgen2  16833  fcfval  17830  nmne0  18242  ovolfsf  18935  lgssq  20686  lgssq2  20687  nv1  21356  adjeq  22629  colinearalg  25097  areacirc  25523  fvopabf4g  25710  exidreslem  25890  hgmapvvlem3  32187
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