![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > 13an22anass | Structured version Visualization version GIF version |
Description: Associative law for four conjunctions with a triple conjunction. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
Ref | Expression |
---|---|
13an22anass | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an2anr 635 | . . 3 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜑)) ↔ ((𝜒 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃))) | |
2 | an2anr 635 | . . . 4 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) ↔ ((𝜒 ∧ 𝜑) ∧ (𝜓 ∧ 𝜃))) | |
3 | an4 654 | . . . 4 ⊢ (((𝜒 ∧ 𝜑) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜒 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃))) | |
4 | 2, 3 | bitri 274 | . . 3 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) ↔ ((𝜒 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃))) |
5 | an43 656 | . . 3 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃))) | |
6 | 1, 4, 5 | 3bitr2ri 299 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜑))) |
7 | 3an4anass 1105 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜑) ↔ ((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜑))) | |
8 | ancom 461 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜑) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃))) | |
9 | 6, 7, 8 | 3bitr2ri 299 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 ∧ w3a 1087 |
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 397 df-3an 1089 |
This theorem is referenced by: ressply1mon1p 32652 |
Copyright terms: Public domain | W3C validator |