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

Theorem 3anrot 970
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 969 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
3 df-3an 967 . 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 965
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 967
This theorem is referenced by:  3ancomb  974  3anrev  976  3simpc  987  an33rean  1332  wefrc  4719  ordelord  4746  fr3nr  6396  omword  7014  nnmcan  7078  pmtr3ncomlem1  15984  srgrmhm  16640  isphld  18088  ordtbaslem  18797  psmettri2  19890  xmetpsmet  19928  comet  20093  cphassr  20735  srabn  20877  lgsdi  22676  colinearalglem2  23158  nb3grapr  23366  nb3grapr2  23367  nb3gra2nb  23368  cusgra3v  23377  dipassr  24251  brapply  27974  brrestrict  27985  dfrdg4  27986  cgrid2  28039  cgr3permute3  28083  cgr3permute2  28085  cgr3permute4  28086  cgr3permute5  28087  colinearperm1  28098  colinearperm3  28099  colinearperm2  28100  colinearperm4  28101  colinearperm5  28102  colinearxfr  28111  endofsegid  28121  colinbtwnle  28154  broutsideof2  28158  dmncan2  28882  f13dfv  30152  frgra3v  30599  lincvalpr  30957  alimp-no-surprise  31138  uunTT1p2  31533  uunT11p1  31535  uunT12p2  31539  uunT12p4  31541  3anidm12p2  31545  uun2221p1  31552  en3lplem2VD  31585  bnj170  31691  bnj290  31703  bnj545  31893  bnj571  31904  bnj594  31910  isltrn2N  33769
  Copyright terms: Public domain W3C validator