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

Theorem 3anrot 996
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 456 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ps  /\  ch )  /\  ph ) )
2 3anass 995 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
3 df-3an 993 . 2  |-  ( ( ps  /\  ch  /\  ph )  <->  ( ( ps 
/\  ch )  /\  ph ) )
41, 2, 33bitr4i 285 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 375    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  3ancomb  1000  3anrev  1002  3simpc  1013  wefrc  4850  ordelord  5468  f13dfv  6203  fr3nr  6638  omword  7302  nnmcan  7366  ncoprmlnprm  14732  pmtr3ncomlem1  17169  srgrmhm  17824  isphld  19276  ordtbaslem  20259  xmetpsmet  21418  comet  21583  cphassr  22244  srabn  22382  lgsdi  24316  colopp  24867  colinearalglem2  24993  nb3grapr  25237  nb3grapr2  25238  nb3gra2nb  25239  cusgra3v  25248  frgra3v  25786  dipassr  26543  bnj170  29553  bnj290  29565  bnj545  29756  bnj571  29767  bnj594  29773  brapply  30755  brrestrict  30766  dfrdg4  30768  cgrid2  30820  cgr3permute3  30864  cgr3permute2  30866  cgr3permute4  30867  cgr3permute5  30868  colinearperm1  30879  colinearperm3  30880  colinearperm2  30881  colinearperm4  30882  colinearperm5  30883  colinearxfr  30892  endofsegid  30902  colinbtwnle  30935  broutsideof2  30939  dmncan2  32356  isltrn2N  33731  uunTT1p2  37223  uunT11p1  37225  uunT12p2  37229  uunT12p4  37231  3anidm12p2  37235  uun2221p1  37242  en3lplem2VD  37281  usgr2edg1  39438  nb3grpr  39602  nb3grpr2  39603  nb3gr2nb  39604  cplgr3v  39648  lincvalpr  40580  alimp-no-surprise  40889
  Copyright terms: Public domain W3C validator