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 ( ( ( ( 𝜑𝜓 ) ∧ 𝜒 ) ∧ ( ( 𝜑𝜃 ) ∧ 𝜏 ) ) ↔ ( ( 𝜓𝜃 ) ∧ ( 𝜑 ∧ ( 𝜒𝜏 ) ) ) )