Theorem wl-embant

Description: A true wff can always be added as a nested antecedent to an antecedent. Note: this theorem is intuitionistically valid. (Contributed by Wolf Lammen, 4-Oct-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	wl-embant.1	|- ph
	wl-embant.2	|- ( ps -> ch )
Assertion	wl-embant	|- ( ( ph -> ps ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		wl-embant.1	|- ph
2		wl-embant.2	|- ( ps -> ch )
3	2	imim2i	|- ( ( ph -> ps ) -> ( ph -> ch ) )
4	1 3	mpi	|- ( ( ph -> ps ) -> ch )