![]() |
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 1482 2reu5lem3 3766 snopeqop 5516 dff1o2 6854 ixxun 13400 elfz1b 13630 mreexexlem4d 17692 unocv 21716 iunocv 21717 iscvsp 25175 mbfmax 25698 ulm2 26443 iswwlks 29866 wwlksnfi 29936 eclclwwlkn1 30104 clwwlknon2x 30132 bnj548 34890 pridlnr 38023 brres2 38250 xrninxp 38374 sineq0ALT 44935 elbigo 48401 |
Copyright terms: Public domain | W3C validator |