|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > 3anan12 | Structured version Visualization version GIF version | ||
| Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised to shorten 3ancoma 1097 by Wolf Lammen, 5-Jun-2022.) | 
| Ref | Expression | 
|---|---|
| 3anan12 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | 3anass 1094 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
| 2 | an12 645 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
| 3 | 1, 2 | bitri 275 | 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: 3ancoma 1097 an33rean 1484 2reu5lem3 3762 snopeqop 5510 dff1o2 6852 ixxun 13404 elfz1b 13634 mreexexlem4d 17691 unocv 21699 iunocv 21700 iscvsp 25162 mbfmax 25685 ulm2 26429 iswwlks 29857 wwlksnfi 29927 eclclwwlkn1 30095 clwwlknon2x 30123 bnj548 34912 pridlnr 38044 brres2 38270 xrninxp 38394 sineq0ALT 44962 elbigo 48477 | 
| Copyright terms: Public domain | W3C validator |