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

Theorem 3anrot 1036
Description: Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
3anrot ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))

Proof of Theorem 3anrot
StepHypRef Expression
1 ancom 465 . 2 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜓𝜒) ∧ 𝜑))
2 3anass 1035 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
3 df-3an 1033 . 2 ((𝜓𝜒𝜑) ↔ ((𝜓𝜒) ∧ 𝜑))
41, 2, 33bitr4i 291 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  3ancomb  1040  3anrev  1042  3simpc  1053  wefrc  5022  ordelord  5648  f13dfv  6408  fr3nr  6849  omword  7515  nnmcan  7579  modmulconst  14800  ncoprmlnprm  15223  pmtr3ncomlem1  17665  srgrmhm  18308  isphld  19766  ordtbaslem  20750  xmetpsmet  21911  comet  22076  cphassr  22765  srabn  22909  lgsdi  24804  colopp  25407  colinearalglem2  25533  nb3grapr  25776  nb3grapr2  25777  nb3gra2nb  25778  cusgra3v  25787  frgra3v  26323  dipassr  26879  bnj170  29811  bnj290  29823  bnj545  30013  bnj571  30024  bnj594  30030  brapply  31009  brrestrict  31020  dfrdg4  31022  cgrid2  31074  cgr3permute3  31118  cgr3permute2  31120  cgr3permute4  31121  cgr3permute5  31122  colinearperm1  31133  colinearperm3  31134  colinearperm2  31135  colinearperm4  31136  colinearperm5  31137  colinearxfr  31146  endofsegid  31156  colinbtwnle  31189  broutsideof2  31193  dmncan2  32840  isltrn2N  34218  ntrneikb  37206  ntrneixb  37207  uunTT1p2  37837  uunT11p1  37839  uunT12p2  37843  uunT12p4  37845  3anidm12p2  37849  uun2221p1  37856  en3lplem2VD  37895  umgr2edg1  40430  nb3grpr  40602  nb3grpr2  40603  nb3gr2nb  40604  cplgr3v  40649  frgr3v  41437  lincvalpr  41993  alimp-no-surprise  42289
  Copyright terms: Public domain W3C validator