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.) |
Ref | Expression |
---|---|
3anan12 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ancoma 1045 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) | |
2 | 3anass 1042 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | bitri 264 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 384 ∧ w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: an33rean 1446 2reu5lem3 3415 snopeqop 4969 fncnv 5962 dff1o2 6142 ixxun 12191 elfz1b 12409 mreexexlem4d 16307 unocv 20024 iunocv 20025 iscvsp 22928 mbfmax 23416 ulm2 24139 iswwlks 26728 wwlksnfi 26801 eclclwwlksn1 26952 numclwlk1lem2f1 27227 bnj548 30967 pridlnr 33835 brres2 34035 sineq0ALT 39173 elbigo 42345 |
Copyright terms: Public domain | W3C validator |