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

Theorem 3anrot 978
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 450 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ps  /\  ch )  /\  ph ) )
2 3anass 977 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
3 df-3an 975 . 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 369    /\ w3a 973
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 371  df-3an 975
This theorem is referenced by:  3ancomb  982  3anrev  984  3simpc  995  an33rean  1342  wefrc  4873  ordelord  4900  f13dfv  6166  fr3nr  6593  omword  7216  nnmcan  7280  pmtr3ncomlem1  16294  srgrmhm  16975  isphld  18456  ordtbaslem  19455  psmettri2  20548  xmetpsmet  20586  comet  20751  cphassr  21393  srabn  21535  lgsdi  23335  colinearalglem2  23886  nb3grapr  24129  nb3grapr2  24130  nb3gra2nb  24131  cusgra3v  24140  frgra3v  24678  dipassr  25437  brapply  29165  brrestrict  29176  dfrdg4  29177  cgrid2  29230  cgr3permute3  29274  cgr3permute2  29276  cgr3permute4  29277  cgr3permute5  29278  colinearperm1  29289  colinearperm3  29290  colinearperm2  29291  colinearperm4  29292  colinearperm5  29293  colinearxfr  29302  endofsegid  29312  colinbtwnle  29345  broutsideof2  29349  dmncan2  30077  lincvalpr  32092  alimp-no-surprise  32277  uunTT1p2  32672  uunT11p1  32674  uunT12p2  32678  uunT12p4  32680  3anidm12p2  32684  uun2221p1  32691  en3lplem2VD  32724  bnj170  32830  bnj290  32842  bnj545  33032  bnj571  33043  bnj594  33049  isltrn2N  34916
  Copyright terms: Public domain W3C validator