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

Theorem 3anrot 941
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 438 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ps  /\  ch )  /\  ph ) )
2 3anass 940 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
3 df-3an 938 . 2  |-  ( ( ps  /\  ch  /\  ph )  <->  ( ( ps 
/\  ch )  /\  ph ) )
41, 2, 33bitr4i 269 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3ancomb  945  3anrev  947  3simpc  956  wefrc  4576  ordelord  4603  fr3nr  4760  omword  6813  nnmcan  6877  latlem12  14507  isphld  16885  ordtbaslem  17252  psmettri2  18340  xmetpsmet  18378  comet  18543  cphassr  19174  srabn  19314  lgsdi  21116  nb3grapr  21462  nb3grapr2  21463  nb3gra2nb  21464  cusgra3v  21473  dipassr  22347  brapply  25783  brrestrict  25794  dfrdg4  25795  colinearalglem2  25846  cgrid2  25937  cgr3permute3  25981  cgr3permute2  25983  cgr3permute4  25984  cgr3permute5  25985  colinearperm1  25996  colinearperm3  25997  colinearperm2  25998  colinearperm4  25999  colinearperm5  26000  colinearxfr  26009  endofsegid  26019  colinbtwnle  26052  broutsideof2  26056  dmncan2  26687  f13dfv  28081  frgra3v  28392  uunTT1p2  28907  uunT11p1  28909  uunT12p2  28913  uunT12p4  28915  3anidm12p2  28919  uun2221p1  28926  en3lplem2VD  28956  bnj170  29062  bnj290  29074  bnj545  29266  bnj571  29277  bnj594  29283  isltrn2N  30917
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator