Theorem neg_or_dist_and ≪ | index | src | ≫

\neg\or分配\and

theorem neg_or_dist_and (A B: wff): $ \neg (A \or B) \iff \neg A \and \neg B $;
StepHypRefExpression
1 iff_eliml 
((\neg A \imp B \iff \neg A \imp \neg \neg B) \iff \neg (\neg A \imp B) \iff \neg (\neg A \imp \neg \neg B)) \imp
  (\neg A \imp B \iff \neg A \imp \neg \neg B) \imp
  (\neg (\neg A \imp B) \iff \neg (\neg A \imp \neg \neg B))
2 iff_alloc_neg 
(\neg A \imp B \iff \neg A \imp \neg \neg B) \iff \neg (\neg A \imp B) \iff \neg (\neg A \imp \neg \neg B)
3 1, 2 ax_mp 
(\neg A \imp B \iff \neg A \imp \neg \neg B) \imp (\neg (\neg A \imp B) \iff \neg (\neg A \imp \neg \neg B))
4 iff_tran 
(\neg A \imp B \iff \neg B \imp A) \imp (\neg B \imp A \iff \neg A \imp \neg \neg B) \imp (\neg A \imp B \iff \neg A \imp \neg \neg B)
5 neg_imp_perm 
\neg A \imp B \iff \neg B \imp A
6 4, 5 ax_mp 
(\neg B \imp A \iff \neg A \imp \neg \neg B) \imp (\neg A \imp B \iff \neg A \imp \neg \neg B)
7 imp_allocrev_neg 
\neg B \imp A \iff \neg A \imp \neg \neg B
8 6, 7 ax_mp 
\neg A \imp B \iff \neg A \imp \neg \neg B
9 3, 8 ax_mp 
\neg (\neg A \imp B) \iff \neg (\neg A \imp \neg \neg B)
10 9 conv or 
\neg (A \or B) \iff \neg (\neg A \imp \neg \neg B)
11 10 conv and 
\neg (A \or B) \iff \neg A \and \neg B

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)