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

Theorem biimp3ar 1329
Description: Infer implication from a logical equivalence. Similar to biimpar 485. (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 622 . 2  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
323imp 1190 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  rmoi  3432  brelrng  5230  div2sub  10365  ssfzo12  11869  modltm1p1mod  12003  abssubge0  13119  qredeu  14103  abvne0  17259  slesolinvbi  18950  basgen2  19257  fcfval  20269  nmne0  20873  ovolfsf  21618  lgssq  23338  lgssq2  23339  colinearalg  23889  nv1  25255  adjeq  26530  areacirc  29689  fvopabf4g  29814  exidreslem  29942  iocmbl  30785  ssfz12  31799  iunconlem2  32815  hgmapvvlem3  36725
  Copyright terms: Public domain W3C validator