Theorem imp_elimls_ex ≪ | index | src | ≫

\imp左侧消除\ex

theorem imp_elimls_ex {x: set} (A B: wff x): $ (\ex x A \imp B) \imp A \imp B $;

Step	Hyp	Ref	Expression
1		imp_introrevr_imp	(A \imp \ex x A) \imp (\ex x A \imp B) \imp A \imp B
2		ex_intro	A \imp \ex x A
3	1, 2	ax_mp	(\ex x A \imp B) \imp A \imp B

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_5, ax_6, ax_7, ax_12)