Description: Associative law for four conjunctions with a triple conjunction. (Contributed by Thierry Arnoux, 21-Jan-2025) (Proof shortened by Wolf Lammen, 31-Oct-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 13an22anass | |- ( ( ph /\ ( ps /\ ch /\ th ) ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3anass | |- ( ( ps /\ ch /\ th ) <-> ( ps /\ ( ch /\ th ) ) ) |
|
| 2 | 1 | bianass | |- ( ( ph /\ ( ps /\ ch /\ th ) ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) ) ) |