Metamath Proof Explorer

Theorem 4an21

Description: Rearrangement of 4 conjuncts with a triple conjunction. (Contributed by AV, 4-Mar-2022)

Ref Expression
Assertion 4an21 ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ∧ 𝜃 ) ↔ ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ∧ 𝜃 ) ) )

Proof

Step Hyp Ref Expression
1 3anass ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ∧ 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) )
2 ancom ⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜓 ∧ 𝜑 ) )
3 2 anbi1i ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ( ( 𝜓 ∧ 𝜑 ) ∧ ( 𝜒 ∧ 𝜃 ) ) )
4 anass ⊢ ( ( ( 𝜓 ∧ 𝜑 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ( 𝜓 ∧ ( 𝜑 ∧ ( 𝜒 ∧ 𝜃 ) ) ) )
5 3anass ⊢ ( ( 𝜑 ∧ 𝜒 ∧ 𝜃 ) ↔ ( 𝜑 ∧ ( 𝜒 ∧ 𝜃 ) ) )
6 5 bicomi ⊢ ( ( 𝜑 ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ( 𝜑 ∧ 𝜒 ∧ 𝜃 ) )
7 6 anbi2i ⊢ ( ( 𝜓 ∧ ( 𝜑 ∧ ( 𝜒 ∧ 𝜃 ) ) ) ↔ ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ∧ 𝜃 ) ) )
8 4 7 bitri ⊢ ( ( ( 𝜓 ∧ 𝜑 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ∧ 𝜃 ) ) )
9 3 8 bitri ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ∧ 𝜃 ) ) )
10 1 9 bitri ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ∧ 𝜃 ) ↔ ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ∧ 𝜃 ) ) )