| 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 1098 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) | |
| 2 | 3ancomb 1099 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) | |
| 3 | 1, 2 | bitri 275 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: 3anrev 1101 wefrc 5679 ordelord 6406 f13dfv 7294 fr3nr 7792 omword 8608 nnmcan 8672 modmulconst 16325 ncoprmlnprm 16765 issubmndb 18818 pmtr3ncomlem1 19491 srgrmhm 20219 isphld 21672 ordtbaslem 23196 xmetpsmet 24358 comet 24526 cphassr 25246 srabn 25394 lgsdi 27378 divsclw 28220 colopp 28777 colinearalglem2 28922 umgr2edg1 29228 nb3grpr 29399 nb3grpr2 29400 nb3gr2nb 29401 cplgr3v 29452 frgr3v 30294 dipassr 30865 bnj170 34712 bnj290 34724 bnj545 34909 bnj571 34920 bnj594 34926 brapply 35939 brrestrict 35950 dfrdg4 35952 cgrid2 36004 cgr3permute3 36048 cgr3permute2 36050 cgr3permute4 36051 cgr3permute5 36052 colinearperm1 36063 colinearperm3 36064 colinearperm2 36065 colinearperm4 36066 colinearperm5 36067 colinearxfr 36076 endofsegid 36086 colinbtwnle 36119 broutsideof2 36123 dmncan2 38084 isltrn2N 40122 oeord2com 43324 uunTT1p2 44815 uunT11p1 44817 uunT12p2 44821 uunT12p4 44823 3anidm12p2 44827 uun2221p1 44834 en3lplem2VD 44864 grtriproplem 47906 grtrif1o 47909 lincvalpr 48335 alimp-no-surprise 49300 |
| Copyright terms: Public domain | W3C validator |