Theorem negiff_boole_def ≪ | index | src | ≫

\neg\iff布尔等价式

theorem negiff_boole_def (A B: wff):
  $ \neg (A \iff B) \iff A \and \neg B \or (B \and \neg A) $;
StepHypRefExpression
1 iff_tran 
(\neg (A \iff B) \iff \neg (A \imp B) \or \neg (B \imp A)) \imp
  (\neg (A \imp B) \or \neg (B \imp A) \iff A \and \neg B \or (B \and \neg A)) \imp
  (\neg (A \iff B) \iff A \and \neg B \or (B \and \neg A))
2 iff_tran 
(\neg \neg ((A \imp B) \imp \neg (B \imp A)) \iff (A \imp B) \imp \neg (B \imp A)) \imp
  ((A \imp B) \imp \neg (B \imp A) \iff \neg \neg (A \imp B) \imp \neg (B \imp A)) \imp
  (\neg \neg ((A \imp B) \imp \neg (B \imp A)) \iff \neg \neg (A \imp B) \imp \neg (B \imp A))
3 iff_symm 
((A \imp B) \imp \neg (B \imp A) \iff \neg \neg ((A \imp B) \imp \neg (B \imp A))) \imp
  (\neg \neg ((A \imp B) \imp \neg (B \imp A)) \iff (A \imp B) \imp \neg (B \imp A))
4 negneg_alloc 
(A \imp B) \imp \neg (B \imp A) \iff \neg \neg ((A \imp B) \imp \neg (B \imp A))
5 3, 4 ax_mp 
\neg \neg ((A \imp B) \imp \neg (B \imp A)) \iff (A \imp B) \imp \neg (B \imp A)
6 2, 5 ax_mp 
((A \imp B) \imp \neg (B \imp A) \iff \neg \neg (A \imp B) \imp \neg (B \imp A)) \imp
  (\neg \neg ((A \imp B) \imp \neg (B \imp A)) \iff \neg \neg (A \imp B) \imp \neg (B \imp A))
7 iff_intror_imp 
(A \imp B \iff \neg \neg (A \imp B)) \imp ((A \imp B) \imp \neg (B \imp A) \iff \neg \neg (A \imp B) \imp \neg (B \imp A))
8 negneg_alloc 
A \imp B \iff \neg \neg (A \imp B)
9 7, 8 ax_mp 
(A \imp B) \imp \neg (B \imp A) \iff \neg \neg (A \imp B) \imp \neg (B \imp A)
10 6, 9 ax_mp 
\neg \neg ((A \imp B) \imp \neg (B \imp A)) \iff \neg \neg (A \imp B) \imp \neg (B \imp A)
11 10 conv and 
\neg ((A \imp B) \and (B \imp A)) \iff \neg \neg (A \imp B) \imp \neg (B \imp A)
12 11 conv or 
\neg ((A \imp B) \and (B \imp A)) \iff \neg (A \imp B) \or \neg (B \imp A)
13 12 conv iff 
\neg (A \iff B) \iff \neg (A \imp B) \or \neg (B \imp A)
14 1, 13 ax_mp 
(\neg (A \imp B) \or \neg (B \imp A) \iff A \and \neg B \or (B \and \neg A)) \imp (\neg (A \iff B) \iff A \and \neg B \or (B \and \neg A))
15 iff_simintro_or 
(\neg (A \imp B) \iff A \and \neg B) \imp (\neg (B \imp A) \iff B \and \neg A) \imp (\neg (A \imp B) \or \neg (B \imp A) \iff A \and \neg B \or (B \and \neg A))
16 negimp_boole_def 
\neg (A \imp B) \iff A \and \neg B
17 15, 16 ax_mp 
(\neg (B \imp A) \iff B \and \neg A) \imp (\neg (A \imp B) \or \neg (B \imp A) \iff A \and \neg B \or (B \and \neg A))
18 negimp_boole_def 
\neg (B \imp A) \iff B \and \neg A
19 17, 18 ax_mp 
\neg (A \imp B) \or \neg (B \imp A) \iff A \and \neg B \or (B \and \neg A)
20 14, 19 ax_mp 
\neg (A \iff B) \iff A \and \neg B \or (B \and \neg A)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)