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	⊢ 𝜑
	wl-embant.2	⊢ ( 𝜓 → 𝜒 )
Assertion	wl-embant	⊢ ( ( 𝜑 → 𝜓 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		wl-embant.1	⊢ 𝜑
2		wl-embant.2	⊢ ( 𝜓 → 𝜒 )
3	2	imim2i	⊢ ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) )
4	1 3	mpi	⊢ ( ( 𝜑 → 𝜓 ) → 𝜒 )