Theorem an3

Description: A rearrangement of conjuncts. (Contributed by Rodolfo Medina, 25-Sep-2010)

	Ref	Expression
Assertion	an3	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) → ( 𝜑 ∧ 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		an43	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜓 ∧ 𝜒 ) ) )
2	1	simplbi	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) → ( 𝜑 ∧ 𝜃 ) )