Description: Associative law for four conjunctions with a triple conjunction. (Contributed by Alexander van der Vekens, 24-Jun-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | 3an4anass | ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an | ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ) | |
2 | 1 | anbi1i | ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) ) |
3 | anass | ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ) | |
4 | 2 3 | bitri | ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ) |