Theorem embantd

Description: Deduction embedding an antecedent. (Contributed by Wolf Lammen, 4-Oct-2013)

	Ref	Expression
Hypotheses	embantd.1	|- ( ph -> ps )
	embantd.2	|- ( ph -> ( ch -> th ) )
Assertion	embantd	|- ( ph -> ( ( ps -> ch ) -> th ) )

Proof

Step	Hyp	Ref	Expression
1		embantd.1	|- ( ph -> ps )
2		embantd.2	|- ( ph -> ( ch -> th ) )
3	2	imim2d	|- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) )
4	1 3	mpid	|- ( ph -> ( ( ps -> ch ) -> th ) )