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

Theorem 3anrot 965
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 448 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ps  /\  ch )  /\  ph ) )
2 3anass 964 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
3 df-3an 962 . 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 960
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 962
This theorem is referenced by:  3ancomb  969  3anrev  971  3simpc  982  an33rean  1327  wefrc  4710  ordelord  4737  fr3nr  6390  omword  7005  nnmcan  7069  pmtr3ncomlem1  15972  srgrmhm  16625  isphld  18042  ordtbaslem  18751  psmettri2  19844  xmetpsmet  19882  comet  20047  cphassr  20689  srabn  20831  lgsdi  22630  colinearalglem2  23088  nb3grapr  23296  nb3grapr2  23297  nb3gra2nb  23298  cusgra3v  23307  dipassr  24181  brapply  27898  brrestrict  27909  dfrdg4  27910  cgrid2  27963  cgr3permute3  28007  cgr3permute2  28009  cgr3permute4  28010  cgr3permute5  28011  colinearperm1  28022  colinearperm3  28023  colinearperm2  28024  colinearperm4  28025  colinearperm5  28026  colinearxfr  28035  endofsegid  28045  colinbtwnle  28078  broutsideof2  28082  dmncan2  28802  f13dfv  30072  frgra3v  30519  lincvalpr  30793  alimp-no-surprise  30972  uunTT1p2  31362  uunT11p1  31364  uunT12p2  31368  uunT12p4  31370  3anidm12p2  31374  uun2221p1  31381  en3lplem2VD  31414  bnj170  31520  bnj290  31532  bnj545  31722  bnj571  31733  bnj594  31739  isltrn2N  33486
  Copyright terms: Public domain W3C validator