Theorem an43

Description: Rearrangement of 4 conjuncts. (Contributed by Rodolfo Medina, 24-Sep-2010) (Proof shortened by Andrew Salmon, 29-Jun-2011)

	Ref	Expression
Assertion	an43	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜓 ∧ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		an42	⊢ ( ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) )
2	1	bicomi	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜓 ∧ 𝜒 ) ) )