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 1038 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) | |
2 | 3anass 1035 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | bitri 263 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: an33rean 1438 2reu5lem3 3382 snopeqop 4894 fncnv 5876 dff1o2 6055 ixxun 12062 mreexexlem4d 16130 unocv 19843 iunocv 19844 iscvsp 22736 mbfmax 23222 ulm2 23943 usgra2wlkspthlem2 26148 wwlknprop 26214 wwlknfi 26266 eclclwwlkn1 26359 numclwwlkovf2 26611 numclwlk1lem2f1 26621 bnj548 30221 pridlnr 33005 sineq0ALT 38195 iswwlks 41039 wwlksnfi 41112 eclclwwlksn1 41259 av-numclwlk1lem2f1 41524 elbigo 42143 |
Copyright terms: Public domain | W3C validator |