Theorem and_imp_insr_or ≪ | index | src | ≫

\imp\and右插入\or

theorem and_imp_insr_or (A B C: wff):
  $ (A \and B \imp C) \imp (A \imp C) \or (B \imp C) $;
StepHypRefExpression
1 neg_elimintror_imp 
\neg B \imp B \imp C
2 1 _hyp_null_complete 
(\neg (A \imp \neg B) \imp C) \and \neg (A \imp C) \imp \neg B \imp B \imp C
3 neg_imp_swap 
(\neg (A \imp \neg B) \imp C) \imp \neg C \imp A \imp \neg B
4 3 _hyp_null_complete 
(\neg (A \imp \neg B) \imp C) \and \neg (A \imp C) \imp (\neg (A \imp \neg B) \imp C) \imp \neg C \imp A \imp \neg B
5 _hyp_null_intro 
(\neg (A \imp \neg B) \imp C) \imp \neg (A \imp \neg B) \imp C
6 5 _hyp_complete 
(\neg (A \imp \neg B) \imp C) \and \neg (A \imp C) \imp \neg (A \imp \neg B) \imp C
7 4, 6 _hyp_mp 
(\neg (A \imp \neg B) \imp C) \and \neg (A \imp C) \imp \neg C \imp A \imp \neg B
8 negimp_splitr_neg 
\neg (A \imp C) \imp \neg C
9 8 _hyp_null_complete 
(\neg (A \imp \neg B) \imp C) \and \neg (A \imp C) \imp \neg (A \imp C) \imp \neg C
10 _hyp_intro 
(\neg (A \imp \neg B) \imp C) \and \neg (A \imp C) \imp \neg (A \imp C)
11 9, 10 _hyp_mp 
(\neg (A \imp \neg B) \imp C) \and \neg (A \imp C) \imp \neg C
12 7, 11 _hyp_mp 
(\neg (A \imp \neg B) \imp C) \and \neg (A \imp C) \imp A \imp \neg B
13 negimp_splitl 
\neg (A \imp C) \imp A
14 13 _hyp_null_complete 
(\neg (A \imp \neg B) \imp C) \and \neg (A \imp C) \imp \neg (A \imp C) \imp A
15 14, 10 _hyp_mp 
(\neg (A \imp \neg B) \imp C) \and \neg (A \imp C) \imp A
16 12, 15 _hyp_mp 
(\neg (A \imp \neg B) \imp C) \and \neg (A \imp C) \imp \neg B
17 2, 16 _hyp_mp 
(\neg (A \imp \neg B) \imp C) \and \neg (A \imp C) \imp B \imp C
18 17 _hyp_rm 
(\neg (A \imp \neg B) \imp C) \imp \neg (A \imp C) \imp B \imp C
19 18 conv and, or 
(A \and B \imp C) \imp (A \imp C) \or (B \imp C)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)