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  4517  ordelord  4544  fr3nr  4700  omword  6749  nnmcan  6813  latlem12  14434  isphld  16808  ordtbaslem  17174  comet  18433  cphassr  19045  srabn  19181  lgsdi  20983  nb3grapr  21328  nb3grapr2  21329  nb3gra2nb  21330  cusgra3v  21339  dipassr  22195  brapply  25501  brrestrict  25512  dfrdg4  25513  colinearalglem2  25560  cgrid2  25651  cgr3permute3  25695  cgr3permute2  25697  cgr3permute4  25698  cgr3permute5  25699  colinearperm1  25710  colinearperm3  25711  colinearperm2  25712  colinearperm4  25713  colinearperm5  25714  colinearxfr  25723  endofsegid  25733  colinbtwnle  25766  broutsideof2  25770  dmncan2  26378  frgra3v  27755  uunTT1p2  28248  uunT11p1  28250  uunT12p2  28254  uunT12p4  28256  3anidm12p2  28260  uun2221p1  28267  en3lplem2VD  28297  bnj170  28400  bnj290  28412  bnj545  28604  bnj571  28615  bnj594  28621  isltrn2N  30234
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