Theorem and_assoc ≪ | index | src | ≫

\and结合

theorem and_assoc (A B C: wff): $ A \and B \and C \iff A \and (B \and C) $;
StepHypRefExpression
1 iff_intro_neg 
(\neg (A \imp \neg B) \imp \neg C \iff A \imp \neg \neg (B \imp \neg C)) \imp
  (\neg (\neg (A \imp \neg B) \imp \neg C) \iff \neg (A \imp \neg \neg (B \imp \neg C)))
2 iff_tran 
(\neg (A \imp \neg B) \imp \neg C \iff A \imp C \imp \neg B) \imp
  (A \imp C \imp \neg B \iff A \imp \neg \neg (B \imp \neg C)) \imp
  (\neg (A \imp \neg B) \imp \neg C \iff A \imp \neg \neg (B \imp \neg C))
3 iff_tran 
(\neg (A \imp \neg B) \imp \neg C \iff C \imp A \imp \neg B) \imp
  (C \imp A \imp \neg B \iff A \imp C \imp \neg B) \imp
  (\neg (A \imp \neg B) \imp \neg C \iff A \imp C \imp \neg B)
4 iff_symm 
(C \imp A \imp \neg B \iff \neg (A \imp \neg B) \imp \neg C) \imp (\neg (A \imp \neg B) \imp \neg C \iff C \imp A \imp \neg B)
5 imp_allocrev_neg 
C \imp A \imp \neg B \iff \neg (A \imp \neg B) \imp \neg C
6 4, 5 ax_mp 
\neg (A \imp \neg B) \imp \neg C \iff C \imp A \imp \neg B
7 3, 6 ax_mp 
(C \imp A \imp \neg B \iff A \imp C \imp \neg B) \imp (\neg (A \imp \neg B) \imp \neg C \iff A \imp C \imp \neg B)
8 imp_imp_perml 
C \imp A \imp \neg B \iff A \imp C \imp \neg B
9 7, 8 ax_mp 
\neg (A \imp \neg B) \imp \neg C \iff A \imp C \imp \neg B
10 2, 9 ax_mp 
(A \imp C \imp \neg B \iff A \imp \neg \neg (B \imp \neg C)) \imp (\neg (A \imp \neg B) \imp \neg C \iff A \imp \neg \neg (B \imp \neg C))
11 iff_introl_imp 
(C \imp \neg B \iff \neg \neg (B \imp \neg C)) \imp (A \imp C \imp \neg B \iff A \imp \neg \neg (B \imp \neg C))
12 iff_tran 
(C \imp \neg B \iff B \imp \neg C) \imp (B \imp \neg C \iff \neg \neg (B \imp \neg C)) \imp (C \imp \neg B \iff \neg \neg (B \imp \neg C))
13 imp_neg_perm 
C \imp \neg B \iff B \imp \neg C
14 12, 13 ax_mp 
(B \imp \neg C \iff \neg \neg (B \imp \neg C)) \imp (C \imp \neg B \iff \neg \neg (B \imp \neg C))
15 negneg_alloc 
B \imp \neg C \iff \neg \neg (B \imp \neg C)
16 14, 15 ax_mp 
C \imp \neg B \iff \neg \neg (B \imp \neg C)
17 11, 16 ax_mp 
A \imp C \imp \neg B \iff A \imp \neg \neg (B \imp \neg C)
18 10, 17 ax_mp 
\neg (A \imp \neg B) \imp \neg C \iff A \imp \neg \neg (B \imp \neg C)
19 1, 18 ax_mp 
\neg (\neg (A \imp \neg B) \imp \neg C) \iff \neg (A \imp \neg \neg (B \imp \neg C))
20 19 conv and 
\neg (A \and B \imp \neg C) \iff \neg (A \imp \neg (B \and C))
21 20 conv and 
A \and B \and C \iff A \and (B \and C)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)