Theorem anim12ci

Description: Variant of anim12i with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

	Ref	Expression
Hypotheses	anim12i.1	$$⊢\phi \to \psi$$
	anim12i.2	$$⊢\chi \to \theta$$
Assertion	anim12ci	$$⊢\left(\phi \wedge \chi \right)\to \left(\theta \wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		anim12i.1	$$⊢\phi \to \psi$$
2		anim12i.2	$$⊢\chi \to \theta$$
3	2 1	anim12i	$$⊢\left(\chi \wedge \phi \right)\to \left(\theta \wedge \psi \right)$$
4	3	ancoms	$$⊢\left(\phi \wedge \chi \right)\to \left(\theta \wedge \psi \right)$$