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

Theorem biimp3ar 1365
Description: Infer implication from a logical equivalence. Similar to biimpar 487. (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 626 . 2  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
323imp 1199 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  rmoi  3392  brelrng  5080  div2sub  10433  ssfzo12  12004  modltm1p1mod  12142  abssubge0  13379  qredeu  14652  abvne0  18043  slesolinvbi  19693  basgen2  19992  fcfval  21035  nmne0  21619  ovolfsf  22411  lgssq  24250  lgssq2  24251  colinearalg  24927  nv1  26291  adjeq  27574  areacirc  31951  fvopabf4g  31961  exidreslem  32089  hgmapvvlem3  35415  iocmbl  36017  iunconlem2  37193  ssfz12  38743  m1modmmod  39598
  Copyright terms: Public domain W3C validator