![]() |
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 1095 by Wolf Lammen, 5-Jun-2022.) |
Ref | Expression |
---|---|
3anan12 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anass 1092 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
2 | an12 643 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | bitri 274 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: 3ancoma 1095 an33rean 1480 2reu5lem3 3751 snopeqop 5512 dff1o2 6848 ixxun 13394 elfz1b 13624 mreexexlem4d 17660 unocv 21676 iunocv 21677 iscvsp 25146 mbfmax 25669 ulm2 26414 iswwlks 29770 wwlksnfi 29840 eclclwwlkn1 30008 clwwlknon2x 30036 bnj548 34742 pridlnr 37737 brres2 37966 xrninxp 38090 sineq0ALT 44613 elbigo 47939 |
Copyright terms: Public domain | W3C validator |