|   | 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 278 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 ∧ 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 207 df-an 396 df-3an 1088 | 
| This theorem is referenced by: 3anrot 1099 elioore 13418 leexp2 14212 swrdswrd 14744 pcgcd 16917 ablsubadd23 19832 ablsubsub23 19843 xmetrtri 24366 phtpcer 25028 ishl2 25405 rusgrprc 29609 clwwlknon2num 30125 ablo32 30569 ablodivdiv 30573 ablodiv32 30575 bnj268 34724 bnj945 34788 bnj944 34953 bnj969 34961 loop1cycl 35143 btwncom 36016 btwnswapid2 36020 btwnouttr 36026 cgr3permute1 36050 colinearperm1 36064 endofsegid 36087 colinbtwnle 36120 broutsideof2 36124 outsideofcom 36130 neificl 37761 lhpexle2 40013 faosnf0.11b 43445 dfsucon 43541 uunTT1p1 44819 uun123 44833 smflimlem4 46794 ichexmpl1 47461 prproropf1o 47499 grtriproplem 47911 grtrif1o 47914 alsi-no-surprise 49370 | 
| Copyright terms: Public domain | W3C validator |