Theorem or_updl ≪ | index | src | ≫

\or左更新

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

Step	Hyp	Ref	Expression
1		imp_imp_swapl	((A \imp C) \imp A \or B \imp C \or B) \imp A \or B \imp (A \imp C) \imp C \or B
2		imp_intror_or	(A \imp C) \imp A \or B \imp C \or B
3	1, 2	ax_mp	A \or B \imp (A \imp C) \imp C \or B

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)