Theorem neg_iff_elim ≪ | index | src | ≫

\neg\iff消除

theorem neg_iff_elim (A B: wff): $ (\neg A \iff \neg B) \imp (A \iff B) $;
StepHypRefExpression
1 iff_comp 
(A \imp B) \imp (B \imp A) \imp (A \iff B)
2 1 _hyp_null_complete 
(\neg A \iff \neg B) \imp (A \imp B) \imp (B \imp A) \imp (A \iff B)
3 neg_imp_elimrev 
(\neg B \imp \neg A) \imp A \imp B
4 3 _hyp_null_complete 
(\neg A \iff \neg B) \imp (\neg B \imp \neg A) \imp A \imp B
5 iff_decompbwd 
(\neg A \iff \neg B) \imp \neg B \imp \neg A
6 5 _hyp_null_complete 
(\neg A \iff \neg B) \imp (\neg A \iff \neg B) \imp \neg B \imp \neg A
7 _hyp_null_intro 
(\neg A \iff \neg B) \imp (\neg A \iff \neg B)
8 6, 7 _hyp_mp 
(\neg A \iff \neg B) \imp \neg B \imp \neg A
9 4, 8 _hyp_mp 
(\neg A \iff \neg B) \imp A \imp B
10 2, 9 _hyp_mp 
(\neg A \iff \neg B) \imp (B \imp A) \imp (A \iff B)
11 neg_imp_elimrev 
(\neg A \imp \neg B) \imp B \imp A
12 11 _hyp_null_complete 
(\neg A \iff \neg B) \imp (\neg A \imp \neg B) \imp B \imp A
13 iff_decomp 
(\neg A \iff \neg B) \imp \neg A \imp \neg B
14 13 _hyp_null_complete 
(\neg A \iff \neg B) \imp (\neg A \iff \neg B) \imp \neg A \imp \neg B
15 14, 7 _hyp_mp 
(\neg A \iff \neg B) \imp \neg A \imp \neg B
16 12, 15 _hyp_mp 
(\neg A \iff \neg B) \imp B \imp A
17 10, 16 _hyp_mp 
(\neg A \iff \neg B) \imp (A \iff B)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)