This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem anan

Description: Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020)

Ref Expression
Assertion anan ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ 𝜏 ) ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜑 ∧ ( 𝜒 ∧ 𝜏 ) ) ) )

Proof

Step Hyp Ref Expression
1 an4 ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ 𝜏 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜃 ) ) ∧ ( 𝜒 ∧ 𝜏 ) ) )
2 anandi ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜃 ) ) )
3 ancom ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ 𝜑 ) )
4 2 3 bitr3i ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜃 ) ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ 𝜑 ) )
5 4 anbi1i ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜃 ) ) ∧ ( 𝜒 ∧ 𝜏 ) ) ↔ ( ( ( 𝜓 ∧ 𝜃 ) ∧ 𝜑 ) ∧ ( 𝜒 ∧ 𝜏 ) ) )
6 anass ⊢ ( ( ( ( 𝜓 ∧ 𝜃 ) ∧ 𝜑 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜑 ∧ ( 𝜒 ∧ 𝜏 ) ) ) )
7 1 5 6 3bitri ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ 𝜏 ) ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜑 ∧ ( 𝜒 ∧ 𝜏 ) ) ) )