Theorem anim12d1

Description: Variant of anim12d where the second implication does not depend on the antecedent. (Contributed by Rodolfo Medina, 12-Oct-2010)

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

Proof

Step	Hyp	Ref	Expression
1		anim12d1.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2		anim12d1.2	$$⊢\theta \to \tau$$
3	2	a1i	$$⊢\phi \to \left(\theta \to \tau \right)$$
4	1 3	anim12d	$$⊢\phi \to \left(\left(\psi \wedge \theta \right)\to \left(\chi \wedge \tau \right)\right)$$