![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3ancomb | Structured version Visualization version GIF version |
Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Revised to shorten 3anrot 1097 by Wolf Lammen, 9-Jun-2022.) |
Ref | Expression |
---|---|
3ancomb | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 1086 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 3anan32 1094 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
3 | 1, 2 | bitr4i 277 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 ∧ 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 395 df-3an 1086 |
This theorem is referenced by: 3anrot 1097 elioore 13408 leexp2 14190 swrdswrd 14713 pcgcd 16880 ablsubadd23 19811 ablsubsub23 19822 xmetrtri 24352 phtpcer 25012 ishl2 25389 rusgrprc 29527 clwwlknon2num 30038 ablo32 30482 ablodivdiv 30486 ablodiv32 30488 bnj268 34554 bnj945 34618 bnj944 34783 bnj969 34791 loop1cycl 34965 btwncom 35838 btwnswapid2 35842 btwnouttr 35848 cgr3permute1 35872 colinearperm1 35886 endofsegid 35909 colinbtwnle 35942 broutsideof2 35946 outsideofcom 35952 neificl 37454 lhpexle2 39709 faosnf0.11b 43094 dfsucon 43190 uunTT1p1 44470 uun123 44484 smflimlem4 46395 ichexmpl1 47041 prproropf1o 47079 alsi-no-surprise 48544 |
Copyright terms: Public domain | W3C validator |