![]() |
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 1098 by Wolf Lammen, 9-Jun-2022.) |
Ref | Expression |
---|---|
3ancomb | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 1087 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 3anan32 1095 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
3 | 1, 2 | bitr4i 277 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 ∧ w3a 1085 |
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 1087 |
This theorem is referenced by: 3anrot 1098 an33reanOLD 1482 elioore 13358 leexp2 14140 swrdswrd 14659 pcgcd 16815 ablsubadd23 19722 ablsubsub23 19733 xmetrtri 24081 phtpcer 24741 ishl2 25118 rusgrprc 29114 clwwlknon2num 29625 ablo32 30069 ablodivdiv 30073 ablodiv32 30075 bnj268 34018 bnj945 34082 bnj944 34247 bnj969 34255 loop1cycl 34426 btwncom 35290 btwnswapid2 35294 btwnouttr 35300 cgr3permute1 35324 colinearperm1 35338 endofsegid 35361 colinbtwnle 35394 broutsideof2 35398 outsideofcom 35404 neificl 36924 lhpexle2 39184 faosnf0.11b 42480 dfsucon 42576 uunTT1p1 43857 uun123 43871 smflimlem4 45788 ichexmpl1 46435 prproropf1o 46473 alsi-no-surprise 47930 |
Copyright terms: Public domain | W3C validator |