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  4403  ordelord  4430  fr3nr  4587  omword  6584  nnmcan  6648  latlem12  14200  isphld  16574  ordtbaslem  16934  comet  18075  cphassr  18663  srabn  18793  lgsdi  20587  dipassr  21440  brapply  24547  brrestrict  24558  dfrdg4  24559  colinearalglem2  24606  cgrid2  24697  cgr3permute3  24741  cgr3permute2  24743  cgr3permute4  24744  cgr3permute5  24745  colinearperm1  24756  colinearperm3  24757  colinearperm2  24758  colinearperm4  24759  colinearperm5  24760  colinearxfr  24769  endofsegid  24779  colinbtwnle  24812  broutsideof2  24816  dmncan2  26804  stoweidlem2  27853  nb3grapr  28288  nb3grapr2  28289  nb3gra2nb  28290  cusgra3v  28298  frgra3v  28425  uunTT1p2  28883  uunT11p1  28885  uunT12p2  28889  uunT12p4  28891  3anidm12p2  28895  uun2221p1  28902  en3lplem2VD  28935  bnj170  29038  bnj290  29050  bnj545  29242  bnj571  29253  bnj594  29259  isltrn2N  30931
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