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

Theorem 3ancomb 982
Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
3ancomb

Proof of Theorem 3ancomb
StepHypRef Expression
1 3ancoma 980 . 2
2 3anrot 978 . 2
31, 2bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\w3a 973
This theorem is referenced by:  3simpb  994  an33rean  1342  elioore  11588  leexp2  12220  swrdswrd  12685  pcgcd  14401  xmetrtri  20858  phtpcer  21495  ishl2  21810  frgra3v  25002  numclwwlkovf2num  25085  ablo32  25288  ablodivdiv  25292  ablodiv32  25294  nvsubsub23  25557  btwncom  29664  btwnswapid2  29668  btwnouttr  29674  cgr3permute1  29698  colinearperm1  29712  endofsegid  29735  colinbtwnle  29768  broutsideof2  29772  outsideofcom  29778  neificl  30246  alsi-no-surprise  33211  uunTT1p1  33591  uun123  33605  bnj268  33761  bnj945  33832  bnj944  33996  bnj969  34004  lhpexle2  35734
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
  Copyright terms: Public domain W3C validator