Theorem or_imp_insr ≪ | index | src | ≫

\imp\or右插入

theorem or_imp_insr (A B C: wff):
  $ (A \or B \imp C) \imp (A \imp C) \or (B \imp C) $;
StepHypRefExpression
1 introl_imp 
C \imp B \imp C
2 1 _hyp_null_complete 
((\neg A \imp B) \imp C) \and \neg (A \imp C) \imp C \imp B \imp C
3 _hyp_null_intro 
((\neg A \imp B) \imp C) \imp (\neg A \imp B) \imp C
4 3 _hyp_complete 
((\neg A \imp B) \imp C) \and \neg (A \imp C) \imp (\neg A \imp B) \imp C
5 intror_neg_imp 
A \imp \neg A \imp B
6 5 _hyp_null_complete 
((\neg A \imp B) \imp C) \and \neg (A \imp C) \imp A \imp \neg A \imp B
7 negimp_splitl 
\neg (A \imp C) \imp A
8 7 _hyp_null_complete 
((\neg A \imp B) \imp C) \and \neg (A \imp C) \imp \neg (A \imp C) \imp A
9 _hyp_intro 
((\neg A \imp B) \imp C) \and \neg (A \imp C) \imp \neg (A \imp C)
10 8, 9 _hyp_mp 
((\neg A \imp B) \imp C) \and \neg (A \imp C) \imp A
11 6, 10 _hyp_mp 
((\neg A \imp B) \imp C) \and \neg (A \imp C) \imp \neg A \imp B
12 4, 11 _hyp_mp 
((\neg A \imp B) \imp C) \and \neg (A \imp C) \imp C
13 2, 12 _hyp_mp 
((\neg A \imp B) \imp C) \and \neg (A \imp C) \imp B \imp C
14 13 _hyp_rm 
((\neg A \imp B) \imp C) \imp \neg (A \imp C) \imp B \imp C
15 14 conv or 
(A \or B \imp C) \imp (A \imp C) \or (B \imp C)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)