Theorem 3anrot 978

Description: Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
3anrot

Proof of Theorem 3anrot

Step	Hyp	Ref	Expression
1		ancom 450	. 2
2		3anass 977	. 2
3		df-3an 975	. 2
4	1, 2, 3	3bitr4i 277	1

Syntax hints:  <->wb 184  /\wa 369  /\w3a 973

This theorem is referenced by:  3ancomb  982  3anrev  984  3simpc  995  wefrc  4878  ordelord  4905  f13dfv  6180  fr3nr  6615  omword  7238  nnmcan  7302  pmtr3ncomlem1  16498  srgrmhm  17187  isphld  18689  ordtbaslem  19689  xmetpsmet  20851  comet  21016  cphassr  21658  srabn  21800  lgsdi  23607  colinearalglem2  24210  nb3grapr  24453  nb3grapr2  24454  nb3gra2nb  24455  cusgra3v  24464  frgra3v  25002  dipassr  25761  brapply  29588  brrestrict  29599  dfrdg4  29600  cgrid2  29653  cgr3permute3  29697  cgr3permute2  29699  cgr3permute4  29700  cgr3permute5  29701  colinearperm1  29712  colinearperm3  29713  colinearperm2  29714  colinearperm4  29715  colinearperm5  29716  colinearxfr  29725  endofsegid  29735  colinbtwnle  29768  broutsideof2  29772  dmncan2  30474  lincvalpr  33019  alimp-no-surprise  33196  uunTT1p2  33592  uunT11p1  33594  uunT12p2  33598  uunT12p4  33600  3anidm12p2  33604  uun2221p1  33611  en3lplem2VD  33644  bnj170  33750  bnj290  33762  bnj545  33953  bnj571  33964  bnj594  33970  isltrn2N  35844

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 975