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

Theorem 3anrot 941
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 438 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ps  /\  ch )  /\  ph ) )
2 3anass 940 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
3 df-3an 938 . 2  |-  ( ( ps  /\  ch  /\  ph )  <->  ( ( ps 
/\  ch )  /\  ph ) )
41, 2, 33bitr4i 269 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3ancomb  945  3anrev  947  3simpc  956  wefrc  4536  ordelord  4563  fr3nr  4719  omword  6772  nnmcan  6836  latlem12  14462  isphld  16840  ordtbaslem  17206  psmettri2  18293  xmetpsmet  18331  comet  18496  cphassr  19127  srabn  19267  lgsdi  21069  nb3grapr  21415  nb3grapr2  21416  nb3gra2nb  21417  cusgra3v  21426  dipassr  22300  brapply  25691  brrestrict  25702  dfrdg4  25703  colinearalglem2  25750  cgrid2  25841  cgr3permute3  25885  cgr3permute2  25887  cgr3permute4  25888  cgr3permute5  25889  colinearperm1  25900  colinearperm3  25901  colinearperm2  25902  colinearperm4  25903  colinearperm5  25904  colinearxfr  25913  endofsegid  25923  colinbtwnle  25956  broutsideof2  25960  dmncan2  26577  f13dfv  27962  frgra3v  28106  uunTT1p2  28616  uunT11p1  28618  uunT12p2  28622  uunT12p4  28624  3anidm12p2  28628  uun2221p1  28635  en3lplem2VD  28665  bnj170  28768  bnj290  28780  bnj545  28972  bnj571  28983  bnj594  28989  isltrn2N  30602
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