Theorem or_imp_splitlsr ≪ | index | src | ≫

\or\imp左侧右拆分

theorem or_imp_splitlsr (A B C: wff): $ (A \or B \imp C) \imp B \imp C $;

Step	Hyp	Ref	Expression
1		imp_tran	((A \or B \imp C) \imp (A \imp C) \and (B \imp C)) \imp ((A \imp C) \and (B \imp C) \imp B \imp C) \imp (A \or B \imp C) \imp B \imp C
2		or_imp_insr_and	(A \or B \imp C) \imp (A \imp C) \and (B \imp C)
3	1, 2	ax_mp	((A \imp C) \and (B \imp C) \imp B \imp C) \imp (A \or B \imp C) \imp B \imp C
4		and_splitr	(A \imp C) \and (B \imp C) \imp B \imp C
5	3, 4	ax_mp	(A \or B \imp C) \imp B \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)