Theorem imp_or_extl ≪ | index | src | ≫

\imp\or左提取

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)