Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3anrot | Structured version Visualization version Unicode version |
Description: Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
3anrot |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom 466 | . 2 | |
2 | 3anass 1042 | . 2 | |
3 | df-3an 1039 | . 2 | |
4 | 1, 2, 3 | 3bitr4i 292 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wa 384 w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: 3ancomb 1047 3anrev 1049 3simpc 1060 wefrc 5108 ordelord 5745 f13dfv 6530 fr3nr 6979 omword 7650 nnmcan 7714 modmulconst 15013 ncoprmlnprm 15436 pmtr3ncomlem1 17893 srgrmhm 18536 isphld 19999 ordtbaslem 20992 xmetpsmet 22153 comet 22318 cphassr 23012 srabn 23156 lgsdi 25059 colopp 25661 colinearalglem2 25787 umgr2edg1 26103 nb3grpr 26284 nb3grpr2 26285 nb3gr2nb 26286 cplgr3v 26331 frgr3v 27139 dipassr 27701 bnj170 30764 bnj290 30776 bnj545 30965 bnj571 30976 bnj594 30982 brapply 32045 brrestrict 32056 dfrdg4 32058 cgrid2 32110 cgr3permute3 32154 cgr3permute2 32156 cgr3permute4 32157 cgr3permute5 32158 colinearperm1 32169 colinearperm3 32170 colinearperm2 32171 colinearperm4 32172 colinearperm5 32173 colinearxfr 32182 endofsegid 32192 colinbtwnle 32225 broutsideof2 32229 dmncan2 33876 isltrn2N 35406 ntrneikb 38392 ntrneixb 38393 uunTT1p2 39022 uunT11p1 39024 uunT12p2 39028 uunT12p4 39030 3anidm12p2 39034 uun2221p1 39041 en3lplem2VD 39079 lincvalpr 42207 alimp-no-surprise 42527 |
Copyright terms: Public domain | W3C validator |