Theorem imp_or_insl ≪ | index | src | ≫

\imp\or左插入

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)