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	|- ( ph -> ( ps -> ch ) )
Assertion	imim1d	|- ( ph -> ( ( ch -> th ) -> ( ps -> th ) ) )

Proof

Step	Hyp	Ref	Expression
1		imim1d.1	|- ( ph -> ( ps -> ch ) )
2		idd	|- ( ph -> ( th -> th ) )
3	1 2	imim12d	|- ( ph -> ( ( ch -> th ) -> ( ps -> th ) ) )