Theorem and_or_distl ≪ | index | src | ≫

\and\or左分配

theorem and_or_distl (A B C: wff):
  $ A \and (B \or C) \iff A \and B \or (A \and C) $;
StepHypRefExpression
1 iff_comp 
(A \and (B \or C) \imp A \and B \or (A \and C)) \imp (A \and B \or (A \and C) \imp A \and (B \or C)) \imp (A \and (B \or C) \iff A \and B \or (A \and C))
2 imp_tran 
(\neg (A \imp \neg (\neg B \imp C)) \imp (A \imp \neg C) \imp \neg (A \imp \neg B)) \imp
  (((A \imp \neg C) \imp \neg (A \imp \neg B)) \imp \neg \neg (A \imp \neg B) \imp \neg (A \imp \neg C)) \imp
  \neg (A \imp \neg (\neg B \imp C)) \imp
  \neg \neg (A \imp \neg B) \imp
  \neg (A \imp \neg C)
3 imp_imp_swapl 
((A \imp \neg C) \imp \neg (A \imp \neg (\neg B \imp C)) \imp \neg (A \imp \neg B)) \imp
  \neg (A \imp \neg (\neg B \imp C)) \imp
  (A \imp \neg C) \imp
  \neg (A \imp \neg B)
4 imp_tran 
((A \imp \neg C) \imp (A \imp \neg B) \imp A \imp \neg (\neg B \imp C)) \imp
  (((A \imp \neg B) \imp A \imp \neg (\neg B \imp C)) \imp \neg (A \imp \neg (\neg B \imp C)) \imp \neg (A \imp \neg B)) \imp
  (A \imp \neg C) \imp
  \neg (A \imp \neg (\neg B \imp C)) \imp
  \neg (A \imp \neg B)
5 imp_tran 
((A \imp \neg C) \imp A \imp \neg B \imp \neg (\neg B \imp C)) \imp
  ((A \imp \neg B \imp \neg (\neg B \imp C)) \imp (A \imp \neg B) \imp A \imp \neg (\neg B \imp C)) \imp
  (A \imp \neg C) \imp
  (A \imp \neg B) \imp
  A \imp
  \neg (\neg B \imp C)
6 imp_introl_imp 
(\neg C \imp \neg B \imp \neg (\neg B \imp C)) \imp (A \imp \neg C) \imp A \imp \neg B \imp \neg (\neg B \imp C)
7 imp_tran 
(\neg C \imp (\neg B \imp C) \imp B) \imp (((\neg B \imp C) \imp B) \imp \neg B \imp \neg (\neg B \imp C)) \imp \neg C \imp \neg B \imp \neg (\neg B \imp C)
8 iff_eliml 
((\neg B \imp C) \imp \neg C \imp B \iff \neg C \imp (\neg B \imp C) \imp B) \imp ((\neg B \imp C) \imp \neg C \imp B) \imp \neg C \imp (\neg B \imp C) \imp B
9 imp_imp_perml 
(\neg B \imp C) \imp \neg C \imp B \iff \neg C \imp (\neg B \imp C) \imp B
10 8, 9 ax_mp 
((\neg B \imp C) \imp \neg C \imp B) \imp \neg C \imp (\neg B \imp C) \imp B
11 neg_imp_swap 
(\neg B \imp C) \imp \neg C \imp B
12 10, 11 ax_mp 
\neg C \imp (\neg B \imp C) \imp B
13 7, 12 ax_mp 
(((\neg B \imp C) \imp B) \imp \neg B \imp \neg (\neg B \imp C)) \imp \neg C \imp \neg B \imp \neg (\neg B \imp C)
14 imp_introrev_neg 
((\neg B \imp C) \imp B) \imp \neg B \imp \neg (\neg B \imp C)
15 13, 14 ax_mp 
\neg C \imp \neg B \imp \neg (\neg B \imp C)
16 6, 15 ax_mp 
(A \imp \neg C) \imp A \imp \neg B \imp \neg (\neg B \imp C)
17 5, 16 ax_mp 
((A \imp \neg B \imp \neg (\neg B \imp C)) \imp (A \imp \neg B) \imp A \imp \neg (\neg B \imp C)) \imp
  (A \imp \neg C) \imp
  (A \imp \neg B) \imp
  A \imp
  \neg (\neg B \imp C)
18 imp_imp_insl 
(A \imp \neg B \imp \neg (\neg B \imp C)) \imp (A \imp \neg B) \imp A \imp \neg (\neg B \imp C)
19 17, 18 ax_mp 
(A \imp \neg C) \imp (A \imp \neg B) \imp A \imp \neg (\neg B \imp C)
20 4, 19 ax_mp 
(((A \imp \neg B) \imp A \imp \neg (\neg B \imp C)) \imp \neg (A \imp \neg (\neg B \imp C)) \imp \neg (A \imp \neg B)) \imp
  (A \imp \neg C) \imp
  \neg (A \imp \neg (\neg B \imp C)) \imp
  \neg (A \imp \neg B)
21 imp_introrev_neg 
((A \imp \neg B) \imp A \imp \neg (\neg B \imp C)) \imp \neg (A \imp \neg (\neg B \imp C)) \imp \neg (A \imp \neg B)
22 20, 21 ax_mp 
(A \imp \neg C) \imp \neg (A \imp \neg (\neg B \imp C)) \imp \neg (A \imp \neg B)
23 3, 22 ax_mp 
\neg (A \imp \neg (\neg B \imp C)) \imp (A \imp \neg C) \imp \neg (A \imp \neg B)
24 2, 23 ax_mp 
(((A \imp \neg C) \imp \neg (A \imp \neg B)) \imp \neg \neg (A \imp \neg B) \imp \neg (A \imp \neg C)) \imp
  \neg (A \imp \neg (\neg B \imp C)) \imp
  \neg \neg (A \imp \neg B) \imp
  \neg (A \imp \neg C)
25 imp_introrev_neg 
((A \imp \neg C) \imp \neg (A \imp \neg B)) \imp \neg \neg (A \imp \neg B) \imp \neg (A \imp \neg C)
26 24, 25 ax_mp 
\neg (A \imp \neg (\neg B \imp C)) \imp \neg \neg (A \imp \neg B) \imp \neg (A \imp \neg C)
27 26 conv or 
\neg (A \imp \neg (B \or C)) \imp \neg (A \imp \neg B) \or \neg (A \imp \neg C)
28 27 conv and 
A \and (B \or C) \imp A \and B \or (A \and C)
29 1, 28 ax_mp 
(A \and B \or (A \and C) \imp A \and (B \or C)) \imp (A \and (B \or C) \iff A \and B \or (A \and C))
30 imp_mergel_neg_imp 
(\neg (A \imp \neg B) \imp \neg (A \imp \neg (\neg B \imp C))) \imp
  (\neg (A \imp \neg C) \imp \neg (A \imp \neg (\neg B \imp C))) \imp
  (\neg \neg (A \imp \neg B) \imp \neg (A \imp \neg C)) \imp
  \neg (A \imp \neg (\neg B \imp C))
31 imp_introrev_neg 
((A \imp \neg (\neg B \imp C)) \imp A \imp \neg B) \imp \neg (A \imp \neg B) \imp \neg (A \imp \neg (\neg B \imp C))
32 imp_introl_imp 
(\neg (\neg B \imp C) \imp \neg B) \imp (A \imp \neg (\neg B \imp C)) \imp A \imp \neg B
33 imp_introrev_neg 
(B \imp \neg B \imp C) \imp \neg (\neg B \imp C) \imp \neg B
34 intror_neg_imp 
B \imp \neg B \imp C
35 33, 34 ax_mp 
\neg (\neg B \imp C) \imp \neg B
36 32, 35 ax_mp 
(A \imp \neg (\neg B \imp C)) \imp A \imp \neg B
37 31, 36 ax_mp 
\neg (A \imp \neg B) \imp \neg (A \imp \neg (\neg B \imp C))
38 30, 37 ax_mp 
(\neg (A \imp \neg C) \imp \neg (A \imp \neg (\neg B \imp C))) \imp
  (\neg \neg (A \imp \neg B) \imp \neg (A \imp \neg C)) \imp
  \neg (A \imp \neg (\neg B \imp C))
39 imp_introrev_neg 
((A \imp \neg (\neg B \imp C)) \imp A \imp \neg C) \imp \neg (A \imp \neg C) \imp \neg (A \imp \neg (\neg B \imp C))
40 imp_introl_imp 
(\neg (\neg B \imp C) \imp \neg C) \imp (A \imp \neg (\neg B \imp C)) \imp A \imp \neg C
41 imp_introrev_neg 
(C \imp \neg B \imp C) \imp \neg (\neg B \imp C) \imp \neg C
42 introl_imp 
C \imp \neg B \imp C
43 41, 42 ax_mp 
\neg (\neg B \imp C) \imp \neg C
44 40, 43 ax_mp 
(A \imp \neg (\neg B \imp C)) \imp A \imp \neg C
45 39, 44 ax_mp 
\neg (A \imp \neg C) \imp \neg (A \imp \neg (\neg B \imp C))
46 38, 45 ax_mp 
(\neg \neg (A \imp \neg B) \imp \neg (A \imp \neg C)) \imp \neg (A \imp \neg (\neg B \imp C))
47 46 conv and 
(\neg (A \and B) \imp A \and C) \imp A \and (\neg B \imp C)
48 47 conv or 
A \and B \or (A \and C) \imp A \and (B \or C)
49 29, 48 ax_mp 
A \and (B \or C) \iff A \and B \or (A \and C)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)