![]() |
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 1095 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) | |
2 | 3ancomb 1096 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) | |
3 | 1, 2 | bitri 275 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ 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 206 df-an 396 df-3an 1086 |
This theorem is referenced by: 3anrev 1098 wefrc 5663 ordelord 6380 f13dfv 7268 fr3nr 7756 omword 8571 nnmcan 8635 modmulconst 16238 ncoprmlnprm 16673 issubmndb 18730 pmtr3ncomlem1 19393 srgrmhm 20127 isphld 21547 ordtbaslem 23047 xmetpsmet 24209 comet 24377 cphassr 25095 srabn 25243 lgsdi 27222 divsclw 28049 colopp 28528 colinearalglem2 28673 umgr2edg1 28976 nb3grpr 29147 nb3grpr2 29148 nb3gr2nb 29149 cplgr3v 29200 frgr3v 30037 dipassr 30608 bnj170 34238 bnj290 34250 bnj545 34435 bnj571 34446 bnj594 34452 brapply 35443 brrestrict 35454 dfrdg4 35456 cgrid2 35508 cgr3permute3 35552 cgr3permute2 35554 cgr3permute4 35555 cgr3permute5 35556 colinearperm1 35567 colinearperm3 35568 colinearperm2 35569 colinearperm4 35570 colinearperm5 35571 colinearxfr 35580 endofsegid 35590 colinbtwnle 35623 broutsideof2 35627 dmncan2 37458 isltrn2N 39504 oeord2com 42642 uunTT1p2 44137 uunT11p1 44139 uunT12p2 44143 uunT12p4 44145 3anidm12p2 44149 uun2221p1 44156 en3lplem2VD 44186 lincvalpr 47379 alimp-no-surprise 48107 |
Copyright terms: Public domain | W3C validator |