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

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

Proof of Theorem 3ancoma
StepHypRef Expression
1 ancom 450 . . 3
21anbi1i 695 . 2
3 df-3an 975 . 2
4 df-3an 975 . 2
52, 3, 43bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  /\w3a 973
This theorem is referenced by:  3ancomb  982  3anrev  984  3anan12  986  3com12  1200  f13dfv  6180  suppssfifsupp  7864  elfzmlbp  11815  elfzo2  11832  pythagtriplem2  14341  pythagtrip  14358  xpsfrnel  14960  fucinv  15342  setcinv  15417  xrsdsreclb  18465  ordthaus  19885  regr1lem2  20241  xmetrtri2  20859  hlcomb  23987  nbgrasym  24439  nb3grapr2  24454  nb3gra2nb  24455  iswwlk  24683  rusgranumwlklem0  24948  frgra3v  25002  ablomuldiv  25291  nvadd12  25516  nvscom  25524  cnvadj  26811  iocinif  27592  cgr3permute1  29698  lineext  29726  colinbtwnle  29768  outsideofcom  29778  linecom  29800  linerflx2  29801  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864  uunT12p3  33599  bnj312  33764  cdlemg33d  36435
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