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  24548  brrestrict  24559  dfrdg4  24560  colinearalglem2  24607  cgrid2  24698  cgr3permute3  24742  cgr3permute2  24744  cgr3permute4  24745  cgr3permute5  24746  colinearperm1  24757  colinearperm3  24758  colinearperm2  24759  colinearperm4  24760  colinearperm5  24761  colinearxfr  24770  endofsegid  24780  colinbtwnle  24813  broutsideof2  24817  dmncan2  26805  stoweidlem2  27854  nb3grapr  28289  nb3grapr2  28290  nb3gra2nb  28291  cusgra3v  28299  frgra3v  28426  uunTT1p2  28884  uunT11p1  28886  uunT12p2  28890  uunT12p4  28892  3anidm12p2  28896  uun2221p1  28903  en3lplem2VD  28936  bnj170  29039  bnj290  29051  bnj545  29243  bnj571  29254  bnj594  29260  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