Theorem imp_intror_or ≪ | index | src | ≫

\or对\imp右引入

theorem imp_intror_or (A B C: wff): $ (A \imp B) \imp A \or C \imp B \or C $;
StepHypRefExpression
1 imp_tran 
((A \imp B) \imp \neg B \imp \neg A) \imp ((\neg B \imp \neg A) \imp (\neg A \imp C) \imp \neg B \imp C) \imp (A \imp B) \imp (\neg A \imp C) \imp \neg B \imp C
2 imp_introrev_neg 
(A \imp B) \imp \neg B \imp \neg A
3 1, 2 ax_mp 
((\neg B \imp \neg A) \imp (\neg A \imp C) \imp \neg B \imp C) \imp (A \imp B) \imp (\neg A \imp C) \imp \neg B \imp C
4 imp_introrevr_imp 
(\neg B \imp \neg A) \imp (\neg A \imp C) \imp \neg B \imp C
5 3, 4 ax_mp 
(A \imp B) \imp (\neg A \imp C) \imp \neg B \imp C
6 5 conv or 
(A \imp B) \imp A \or C \imp B \or C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)