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

Metamath Proof Explorer

Theorem an3

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

		Ref	Expression
	Assertion	an3	$⊢ ((φ \land ψ) \land (χ \land θ)) \to (φ \land θ)$

Step	Hyp	Ref	Expression
1		an43	$⊢ ((φ \land ψ) \land (χ \land θ)) \leftrightarrow ((φ \land θ) \land (ψ \land χ))$
2	1	simplbi	$⊢ ((φ \land ψ) \land (χ \land θ)) \to (φ \land θ)$