Theorem or_assoc ≪ | index | src | ≫

\or结合

theorem or_assoc (A B C: wff): $ A \or B \or C \iff A \or (B \or C) $;
StepHypRefExpression
1 iff_tran 
(\neg (\neg A \imp B) \imp C \iff \neg A \imp \neg C \imp B) \imp
  (\neg A \imp \neg C \imp B \iff \neg A \imp \neg B \imp C) \imp
  (\neg (\neg A \imp B) \imp C \iff \neg A \imp \neg B \imp C)
2 iff_tran 
(\neg (\neg A \imp B) \imp C \iff \neg C \imp \neg A \imp B) \imp
  (\neg C \imp \neg A \imp B \iff \neg A \imp \neg C \imp B) \imp
  (\neg (\neg A \imp B) \imp C \iff \neg A \imp \neg C \imp B)
3 neg_imp_perm 
\neg (\neg A \imp B) \imp C \iff \neg C \imp \neg A \imp B
4 2, 3 ax_mp 
(\neg C \imp \neg A \imp B \iff \neg A \imp \neg C \imp B) \imp (\neg (\neg A \imp B) \imp C \iff \neg A \imp \neg C \imp B)
5 imp_imp_perml 
\neg C \imp \neg A \imp B \iff \neg A \imp \neg C \imp B
6 4, 5 ax_mp 
\neg (\neg A \imp B) \imp C \iff \neg A \imp \neg C \imp B
7 1, 6 ax_mp 
(\neg A \imp \neg C \imp B \iff \neg A \imp \neg B \imp C) \imp (\neg (\neg A \imp B) \imp C \iff \neg A \imp \neg B \imp C)
8 iff_introl_imp 
(\neg C \imp B \iff \neg B \imp C) \imp (\neg A \imp \neg C \imp B \iff \neg A \imp \neg B \imp C)
9 neg_imp_perm 
\neg C \imp B \iff \neg B \imp C
10 8, 9 ax_mp 
\neg A \imp \neg C \imp B \iff \neg A \imp \neg B \imp C
11 7, 10 ax_mp 
\neg (\neg A \imp B) \imp C \iff \neg A \imp \neg B \imp C
12 11 conv or 
\neg (A \or B) \imp C \iff \neg A \imp B \or C
13 12 conv or 
A \or B \or C \iff A \or (B \or C)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)