Theorem anim12ii

Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007) (Proof shortened by Wolf Lammen, 19-Jul-2013)

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

Proof

Step	Hyp	Ref	Expression
1		anim12ii.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2		anim12ii.2	$$⊢\theta \to \left(\psi \to \tau \right)$$
3		pm3.43	$$⊢\left(\left(\psi \to \chi \right)\wedge \left(\psi \to \tau \right)\right)\to \left(\psi \to \left(\chi \wedge \tau \right)\right)$$
4	1 2 3	syl2an	$$⊢\left(\phi \wedge \theta \right)\to \left(\psi \to \left(\chi \wedge \tau \right)\right)$$