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

Theorem 3anrot 939
Description: Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
3anrot  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )

Proof of Theorem 3anrot
StepHypRef Expression
1 ancom 437 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ps  /\  ch )  /\  ph ) )
2 3anass 938 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
3 df-3an 936 . 2  |-  ( ( ps  /\  ch  /\  ph )  <->  ( ( ps 
/\  ch )  /\  ph ) )
41, 2, 33bitr4i 268 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3ancomb  943  3anrev  945  3simpc  954  wefrc  4387  ordelord  4414  fr3nr  4571  omword  6568  nnmcan  6632  latlem12  14184  isphld  16558  ordtbaslem  16918  comet  18059  cphassr  18647  srabn  18777  lgsdi  20571  dipassr  21424  brapply  24477  brrestrict  24487  dfrdg4  24488  colinearalglem2  24535  cgrid2  24626  cgr3permute3  24670  cgr3permute2  24672  cgr3permute4  24673  cgr3permute5  24674  colinearperm1  24685  colinearperm3  24686  colinearperm2  24687  colinearperm4  24688  colinearperm5  24689  colinearxfr  24698  endofsegid  24708  colinbtwnle  24741  broutsideof2  24745  dmncan2  26702  stoweidlem2  27751  frgra3v  28180  uunTT1p2  28570  uunT11p1  28572  uunT12p2  28576  uunT12p4  28578  3anidm12p2  28582  uun2221p1  28589  en3lplem2VD  28620  bnj170  28723  bnj290  28735  bnj545  28927  bnj571  28938  bnj594  28944  isltrn2N  30309
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