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	$$⊢\phi$$
	wl-embant.2	$$⊢\psi \to \chi$$
Assertion	wl-embant	$$⊢\left(\phi \to \psi \right)\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		wl-embant.1	$$⊢\phi$$
2		wl-embant.2	$$⊢\psi \to \chi$$
3	2	imim2i	$$⊢\left(\phi \to \psi \right)\to \left(\phi \to \chi \right)$$
4	1 3	mpi	$$⊢\left(\phi \to \psi \right)\to \chi$$