Theorem imp_or_extr_and ≪ | index | src | ≫

\imp\or右提取\and

theorem imp_or_extr_and (A B C: wff):
  $ (A \imp C) \or (B \imp C) \imp A \and B \imp C $;
StepHypRefExpression
1 neg_imp_tosame 
(\neg C \imp C) \imp C
2 1 _hyp_null_complete 
(A \imp C) \or (B \imp C) \and (A \and B) \imp (\neg C \imp C) \imp C
3 imp_imp_swapl 
(\neg C \imp A \imp C) \imp A \imp \neg C \imp C
4 3 _hyp_null_complete 
(A \imp C) \or (B \imp C) \and (A \and B) \imp (\neg C \imp A \imp C) \imp A \imp \neg C \imp C
5 neg_imp_swap 
(\neg (A \imp C) \imp C) \imp \neg C \imp A \imp C
6 5 _hyp_null_complete 
(A \imp C) \or (B \imp C) \and (A \and B) \imp (\neg (A \imp C) \imp C) \imp \neg C \imp A \imp C
7 imp_imp_swapl 
(\neg (A \imp C) \imp B \imp C) \imp B \imp \neg (A \imp C) \imp C
8 7 _hyp_null_complete 
(A \imp C) \or (B \imp C) \and (A \and B) \imp (\neg (A \imp C) \imp B \imp C) \imp B \imp \neg (A \imp C) \imp C
9 _hyp_null_intro 
(A \imp C) \or (B \imp C) \imp (A \imp C) \or (B \imp C)
10 9 conv or 
(A \imp C) \or (B \imp C) \imp \neg (A \imp C) \imp B \imp C
11 10 _hyp_complete 
(A \imp C) \or (B \imp C) \and (A \and B) \imp \neg (A \imp C) \imp B \imp C
12 8, 11 _hyp_mp 
(A \imp C) \or (B \imp C) \and (A \and B) \imp B \imp \neg (A \imp C) \imp C
13 imp_introlsl_and 
(B \imp B) \imp A \and B \imp B
14 13 _hyp_null_complete 
(A \imp C) \or (B \imp C) \and (A \and B) \imp (B \imp B) \imp A \and B \imp B
15 imp_refl 
B \imp B
16 15 _hyp_null_complete 
(A \imp C) \or (B \imp C) \and (A \and B) \imp B \imp B
17 14, 16 _hyp_mp 
(A \imp C) \or (B \imp C) \and (A \and B) \imp A \and B \imp B
18 _hyp_intro 
(A \imp C) \or (B \imp C) \and (A \and B) \imp A \and B
19 17, 18 _hyp_mp 
(A \imp C) \or (B \imp C) \and (A \and B) \imp B
20 12, 19 _hyp_mp 
(A \imp C) \or (B \imp C) \and (A \and B) \imp \neg (A \imp C) \imp C
21 6, 20 _hyp_mp 
(A \imp C) \or (B \imp C) \and (A \and B) \imp \neg C \imp A \imp C
22 4, 21 _hyp_mp 
(A \imp C) \or (B \imp C) \and (A \and B) \imp A \imp \neg C \imp C
23 imp_introlsr_and 
(A \imp A) \imp A \and B \imp A
24 23 _hyp_null_complete 
(A \imp C) \or (B \imp C) \and (A \and B) \imp (A \imp A) \imp A \and B \imp A
25 imp_refl 
A \imp A
26 25 _hyp_null_complete 
(A \imp C) \or (B \imp C) \and (A \and B) \imp A \imp A
27 24, 26 _hyp_mp 
(A \imp C) \or (B \imp C) \and (A \and B) \imp A \and B \imp A
28 27, 18 _hyp_mp 
(A \imp C) \or (B \imp C) \and (A \and B) \imp A
29 22, 28 _hyp_mp 
(A \imp C) \or (B \imp C) \and (A \and B) \imp \neg C \imp C
30 2, 29 _hyp_mp 
(A \imp C) \or (B \imp C) \and (A \and B) \imp C
31 30 _hyp_rm 
(A \imp C) \or (B \imp C) \imp A \and B \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)