![]() |
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 278 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∧ 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 206 df-an 398 df-3an 1090 |
This theorem is referenced by: 3anrot 1101 an33reanOLD 1485 elioore 13350 leexp2 14132 swrdswrd 14651 pcgcd 16807 ablsubadd23 19673 ablsubsub23 19684 xmetrtri 23843 phtpcer 24493 ishl2 24869 rusgrprc 28827 clwwlknon2num 29338 ablo32 29780 ablodivdiv 29784 ablodiv32 29786 bnj268 33658 bnj945 33722 bnj944 33887 bnj969 33895 loop1cycl 34066 btwncom 34924 btwnswapid2 34928 btwnouttr 34934 cgr3permute1 34958 colinearperm1 34972 endofsegid 34995 colinbtwnle 35028 broutsideof2 35032 outsideofcom 35038 neificl 36559 lhpexle2 38819 faosnf0.11b 42111 dfsucon 42207 uunTT1p1 43488 uun123 43502 smflimlem4 45425 ichexmpl1 46072 prproropf1o 46110 alsi-no-surprise 47745 |
Copyright terms: Public domain | W3C validator |