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

Theorem 3anrot 979
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 448 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ps  /\  ch )  /\  ph ) )
2 3anass 978 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
3 df-3an 976 . 2  |-  ( ( ps  /\  ch  /\  ph )  <->  ( ( ps 
/\  ch )  /\  ph ) )
41, 2, 33bitr4i 277 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  3ancomb  983  3anrev  985  3simpc  996  wefrc  4817  ordelord  5432  f13dfv  6161  fr3nr  6597  omword  7256  nnmcan  7320  pmtr3ncomlem1  16822  srgrmhm  17507  isphld  18987  ordtbaslem  19982  xmetpsmet  21143  comet  21308  cphassr  21950  srabn  22092  lgsdi  23988  colopp  24526  colinearalglem2  24627  nb3grapr  24870  nb3grapr2  24871  nb3gra2nb  24872  cusgra3v  24881  frgra3v  25419  dipassr  26175  bnj170  29077  bnj290  29089  bnj545  29280  bnj571  29291  bnj594  29297  brapply  30276  brrestrict  30287  dfrdg4  30289  cgrid2  30341  cgr3permute3  30385  cgr3permute2  30387  cgr3permute4  30388  cgr3permute5  30389  colinearperm1  30400  colinearperm3  30401  colinearperm2  30402  colinearperm4  30403  colinearperm5  30404  colinearxfr  30413  endofsegid  30423  colinbtwnle  30456  broutsideof2  30460  dmncan2  31756  isltrn2N  33137  uunTT1p2  36616  uunT11p1  36618  uunT12p2  36622  uunT12p4  36624  3anidm12p2  36628  uun2221p1  36635  en3lplem2VD  36674  lincvalpr  38530  alimp-no-surprise  38840
  Copyright terms: Public domain W3C validator