![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3anrot | Structured version Visualization version GIF version |
Description: Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
3anrot | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom 465 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑)) | |
2 | 3anass 1059 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
3 | df-3an 1056 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑)) | |
4 | 1, 2, 3 | 3bitr4i 292 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 ∧ w3a 1054 |
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 385 df-3an 1056 |
This theorem is referenced by: 3ancomb 1064 3anrev 1067 3simpc 1080 wefrc 5137 ordelord 5783 f13dfv 6570 fr3nr 7021 omword 7695 nnmcan 7759 modmulconst 15060 ncoprmlnprm 15483 pmtr3ncomlem1 17939 srgrmhm 18582 isphld 20047 ordtbaslem 21040 xmetpsmet 22200 comet 22365 cphassr 23058 srabn 23202 lgsdi 25104 colopp 25706 colinearalglem2 25832 umgr2edg1 26148 nb3grpr 26328 nb3grpr2 26329 nb3gr2nb 26330 cplgr3v 26387 frgr3v 27255 dipassr 27829 bnj170 30892 bnj290 30904 bnj545 31091 bnj571 31102 bnj594 31108 brapply 32170 brrestrict 32181 dfrdg4 32183 cgrid2 32235 cgr3permute3 32279 cgr3permute2 32281 cgr3permute4 32282 cgr3permute5 32283 colinearperm1 32294 colinearperm3 32295 colinearperm2 32296 colinearperm4 32297 colinearperm5 32298 colinearxfr 32307 endofsegid 32317 colinbtwnle 32350 broutsideof2 32354 dmncan2 34006 isltrn2N 35724 ntrneikb 38709 ntrneixb 38710 uunTT1p2 39339 uunT11p1 39341 uunT12p2 39345 uunT12p4 39347 3anidm12p2 39351 uun2221p1 39358 en3lplem2VD 39393 lincvalpr 42532 alimp-no-surprise 42855 |
Copyright terms: Public domain | W3C validator |