Theorem imim12d

Description: Deduction combining antecedents and consequents. Deduction associated with imim12 and imim12i . (Contributed by NM, 7-Aug-1994) (Proof shortened by Mel L. O'Cat, 30-Oct-2011)

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

Proof

Step	Hyp	Ref	Expression
1		imim12d.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2		imim12d.2	$$⊢\phi \to \left(\theta \to \tau \right)$$
3	2	imim2d	$$⊢\phi \to \left(\left(\chi \to \theta \right)\to \left(\chi \to \tau \right)\right)$$
4	1 3	syl5d	$$⊢\phi \to \left(\left(\chi \to \theta \right)\to \left(\psi \to \tau \right)\right)$$