![]() |
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.) (Proof shortened by Wolf Lammen, 9-Jun-2022.) |
Ref | Expression |
---|---|
3anrot | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ancoma 1091 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) | |
2 | 3ancomb 1092 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) | |
3 | 1, 2 | bitri 276 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ w3a 1080 |
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 208 df-an 397 df-3an 1082 |
This theorem is referenced by: 3anrev 1094 wefrc 5437 ordelord 6088 f13dfv 6896 fr3nr 7350 omword 8046 nnmcan 8110 modmulconst 15474 ncoprmlnprm 15897 pmtr3ncomlem1 18332 srgrmhm 18976 isphld 20480 ordtbaslem 21480 xmetpsmet 22641 comet 22806 cphassr 23499 srabn 23646 lgsdi 25592 colopp 26237 colinearalglem2 26376 umgr2edg1 26676 nb3grpr 26847 nb3grpr2 26848 nb3gr2nb 26849 cplgr3v 26900 frgr3v 27746 dipassr 28314 bnj170 31585 bnj290 31597 bnj545 31783 bnj571 31794 bnj594 31800 brapply 33008 brrestrict 33019 dfrdg4 33021 cgrid2 33073 cgr3permute3 33117 cgr3permute2 33119 cgr3permute4 33120 cgr3permute5 33121 colinearperm1 33132 colinearperm3 33133 colinearperm2 33134 colinearperm4 33135 colinearperm5 33136 colinearxfr 33145 endofsegid 33155 colinbtwnle 33188 broutsideof2 33192 dmncan2 34887 isltrn2N 36787 uunTT1p2 40668 uunT11p1 40670 uunT12p2 40674 uunT12p4 40676 3anidm12p2 40680 uun2221p1 40687 en3lplem2VD 40717 lincvalpr 43953 alimp-no-surprise 44362 |
Copyright terms: Public domain | W3C validator |