![]() |
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 1123 by Wolf Lammen, 9-Jun-2022.) |
Ref | Expression |
---|---|
3ancomb | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 1110 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 3anan32 1119 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
3 | 1, 2 | bitr4i 270 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 385 ∧ w3a 1108 |
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 199 df-an 386 df-3an 1110 |
This theorem is referenced by: 3anrot 1123 3simpbOLD 1182 an33rean 1608 elioore 12450 leexp2 13165 swrdswrd 13744 pcgcd 15911 ablsubsub23 18541 xmetrtri 22484 phtpcer 23118 ishl2 23492 rusgrprc 26831 clwwlknon2num 27435 ablo32 27920 ablodivdiv 27924 ablodiv32 27926 bnj268 31286 bnj945 31352 bnj944 31516 bnj969 31524 btwncom 32625 btwnswapid2 32629 btwnouttr 32635 cgr3permute1 32659 colinearperm1 32673 endofsegid 32696 colinbtwnle 32729 broutsideof2 32733 outsideofcom 32739 neificl 34027 lhpexle2 36022 uunTT1p1 39777 uun123 39791 smflimlem4 41715 alsi-no-surprise 43331 |
Copyright terms: Public domain | W3C validator |