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

Theorem biimp3ar 1284
Description: Infer implication from a logical equivalence. Similar to biimpar 472. (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 606 . 2  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
323imp 1147 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936
This theorem is referenced by:  rmoi  3210  brelrng  5058  div2sub  9795  abssubge0  12086  qredeu  13062  abvne0  15870  basgen2  17009  fcfval  18018  nmne0  18618  ovolfsf  19321  lgssq  21072  lgssq2  21073  nv1  22118  adjeq  23391  colinearalg  25753  areacirc  26187  fvopabf4g  26312  exidreslem  26442  ssfz12  27976  ssfzo12  27990  hgmapvvlem3  32411
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  df-3an 938
  Copyright terms: Public domain W3C validator