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

Theorem biimp3ar 1320
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 1182 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  rmoi  3388  brelrng  5170  div2sub  10260  ssfzo12  11730  modltm1p1mod  11861  abssubge0  12926  qredeu  13904  abvne0  17027  slesolinvbi  18612  basgen2  18719  fcfval  19731  nmne0  20335  ovolfsf  21080  lgssq  22800  lgssq2  22801  colinearalg  23301  nv1  24209  adjeq  25484  areacirc  28630  fvopabf4g  28755  exidreslem  28883  iocmbl  29729  ssfz12  30338  iunconlem2  31974  hgmapvvlem3  35882
  Copyright terms: Public domain W3C validator