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 1099 by Wolf Lammen, 9-Jun-2022.) |
Ref | Expression |
---|---|
3ancomb | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 1088 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 3anan32 1096 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
3 | 1, 2 | bitr4i 277 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 ∧ w3a 1086 |
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 397 df-3an 1088 |
This theorem is referenced by: 3anrot 1099 an33reanOLD 1483 elioore 13109 leexp2 13889 swrdswrd 14418 pcgcd 16579 ablsubsub23 19426 xmetrtri 23508 phtpcer 24158 ishl2 24534 rusgrprc 27957 clwwlknon2num 28469 ablo32 28911 ablodivdiv 28915 ablodiv32 28917 bnj268 32688 bnj945 32753 bnj944 32918 bnj969 32926 loop1cycl 33099 btwncom 34316 btwnswapid2 34320 btwnouttr 34326 cgr3permute1 34350 colinearperm1 34364 endofsegid 34387 colinbtwnle 34420 broutsideof2 34424 outsideofcom 34430 neificl 35911 lhpexle2 38024 dfsucon 41130 uunTT1p1 42414 uun123 42428 smflimlem4 44309 ichexmpl1 44921 prproropf1o 44959 alsi-no-surprise 46500 |
Copyright terms: Public domain | W3C validator |