Theorem iff_intro_neg ≪ | index | src | ≫

\iff引入\neg

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)