Metamath Proof Explorer

Theorem 3com12d

Description: Commutation in consequent. Swap 1st and 2nd. (Contributed by Jeff Hankins, 17-Nov-2009)

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

Step	Hyp	Ref	Expression
1		3com12d.1	$⊢ φ \to (ψ \land χ \land θ)$
2		id	$⊢ (χ \land ψ \land θ) \to (χ \land ψ \land θ)$
3	2	3com12	$⊢ (ψ \land χ \land θ) \to (χ \land ψ \land θ)$
4	1 3	syl	$⊢ φ \to (χ \land ψ \land θ)$