Theorem imim1d

Description: Deduction adding nested consequents. Deduction associated with imim1 and imim1i . (Contributed by NM, 3-Apr-1994) (Proof shortened by Wolf Lammen, 12-Sep-2012)

	Ref	Expression
Hypothesis	imim1d.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
Assertion	imim1d	$$⊢\phi \to \left(\left(\chi \to \theta \right)\to \left(\psi \to \theta \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		imim1d.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2		idd	$$⊢\phi \to \left(\theta \to \theta \right)$$
3	1 2	imim12d	$$⊢\phi \to \left(\left(\chi \to \theta \right)\to \left(\psi \to \theta \right)\right)$$