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 1101 by Wolf Lammen, 9-Jun-2022.) |
Ref | Expression |
---|---|
3ancomb | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 1090 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 3anan32 1098 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
3 | 1, 2 | bitr4i 281 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 ∧ w3a 1088 |
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 210 df-an 400 df-3an 1090 |
This theorem is referenced by: 3anrot 1101 an33reanOLD 1485 elioore 12844 leexp2 13620 swrdswrd 14149 pcgcd 16307 ablsubsub23 19057 xmetrtri 23101 phtpcer 23740 ishl2 24115 rusgrprc 27524 clwwlknon2num 28034 ablo32 28476 ablodivdiv 28480 ablodiv32 28482 bnj268 32250 bnj945 32316 bnj944 32481 bnj969 32489 loop1cycl 32662 btwncom 33946 btwnswapid2 33950 btwnouttr 33956 cgr3permute1 33980 colinearperm1 33994 endofsegid 34017 colinbtwnle 34050 broutsideof2 34054 outsideofcom 34060 neificl 35523 lhpexle2 37636 dfsucon 40668 uunTT1p1 41936 uun123 41950 smflimlem4 43832 ichexmpl1 44439 prproropf1o 44477 alsi-no-surprise 45937 |
Copyright terms: Public domain | W3C validator |