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

Metamath Proof Explorer

Theorem an4s

Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995)

		Ref	Expression
	Hypothesis	an4s.1	$⊢ ((φ \land ψ) \land (χ \land θ)) \to τ$
	Assertion	an4s	$⊢ ((φ \land χ) \land (ψ \land θ)) \to τ$

Step	Hyp	Ref	Expression
1		an4s.1	$⊢ ((φ \land ψ) \land (χ \land θ)) \to τ$
2		an4	$⊢ ((φ \land χ) \land (ψ \land θ)) \leftrightarrow ((φ \land ψ) \land (χ \land θ))$
3	2 1	sylbi	$⊢ ((φ \land χ) \land (ψ \land θ)) \to τ$