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

Theorem 3anrot 1097
Description: Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.) (Proof shortened by Wolf Lammen, 9-Jun-2022.)
Assertion
Ref Expression
3anrot ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))

Proof of Theorem 3anrot
StepHypRef Expression
1 3ancoma 1095 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜑𝜒))
2 3ancomb 1096 . 2 ((𝜓𝜑𝜒) ↔ (𝜓𝜒𝜑))
31, 2bitri 278 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 209  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  3anrev  1098  wefrc  5517  ordelord  6185  f13dfv  7013  fr3nr  7478  omword  8183  nnmcan  8247  modmulconst  15636  ncoprmlnprm  16061  issubmndb  17965  pmtr3ncomlem1  18596  srgrmhm  19282  isphld  20346  ordtbaslem  21796  xmetpsmet  22958  comet  23123  cphassr  23820  srabn  23967  lgsdi  25921  colopp  26566  colinearalglem2  26704  umgr2edg1  27004  nb3grpr  27175  nb3grpr2  27176  nb3gr2nb  27177  cplgr3v  27228  frgr3v  28063  dipassr  28632  bnj170  32076  bnj290  32088  bnj545  32275  bnj571  32286  bnj594  32292  brapply  33507  brrestrict  33518  dfrdg4  33520  cgrid2  33572  cgr3permute3  33616  cgr3permute2  33618  cgr3permute4  33619  cgr3permute5  33620  colinearperm1  33631  colinearperm3  33632  colinearperm2  33633  colinearperm4  33634  colinearperm5  33635  colinearxfr  33644  endofsegid  33654  colinbtwnle  33687  broutsideof2  33691  dmncan2  35508  isltrn2N  37409  uunTT1p2  41488  uunT11p1  41490  uunT12p2  41494  uunT12p4  41496  3anidm12p2  41500  uun2221p1  41507  en3lplem2VD  41537  lincvalpr  44814  alimp-no-surprise  45296
  Copyright terms: Public domain W3C validator