Theorem iff_tran ≪ | index | src | ≫

\iff传递

theorem iff_tran (A B C: wff): $ (A \iff B) \imp (B \iff C) \imp (A \iff C) $;
StepHypRefExpression
1 iff_comp 
(A \imp C) \imp (C \imp A) \imp (A \iff C)
2 1 _hyp_null_complete 
(A \iff B) \and (B \iff C) \imp (A \imp C) \imp (C \imp A) \imp (A \iff C)
3 imp_tran 
(A \imp B) \imp (B \imp C) \imp A \imp C
4 3 _hyp_null_complete 
(A \iff B) \and (B \iff C) \imp (A \imp B) \imp (B \imp C) \imp A \imp C
5 iff_decomp 
(A \iff B) \imp A \imp B
6 5 _hyp_null_complete 
(A \iff B) \and (B \iff C) \imp (A \iff B) \imp A \imp B
7 _hyp_null_intro 
(A \iff B) \imp (A \iff B)
8 7 _hyp_complete 
(A \iff B) \and (B \iff C) \imp (A \iff B)
9 6, 8 _hyp_mp 
(A \iff B) \and (B \iff C) \imp A \imp B
10 4, 9 _hyp_mp 
(A \iff B) \and (B \iff C) \imp (B \imp C) \imp A \imp C
11 iff_decomp 
(B \iff C) \imp B \imp C
12 11 _hyp_null_complete 
(A \iff B) \and (B \iff C) \imp (B \iff C) \imp B \imp C
13 _hyp_intro 
(A \iff B) \and (B \iff C) \imp (B \iff C)
14 12, 13 _hyp_mp 
(A \iff B) \and (B \iff C) \imp B \imp C
15 10, 14 _hyp_mp 
(A \iff B) \and (B \iff C) \imp A \imp C
16 2, 15 _hyp_mp 
(A \iff B) \and (B \iff C) \imp (C \imp A) \imp (A \iff C)
17 imp_tran 
(C \imp B) \imp (B \imp A) \imp C \imp A
18 17 _hyp_null_complete 
(A \iff B) \and (B \iff C) \imp (C \imp B) \imp (B \imp A) \imp C \imp A
19 iff_decompbwd 
(B \iff C) \imp C \imp B
20 19 _hyp_null_complete 
(A \iff B) \and (B \iff C) \imp (B \iff C) \imp C \imp B
21 20, 13 _hyp_mp 
(A \iff B) \and (B \iff C) \imp C \imp B
22 18, 21 _hyp_mp 
(A \iff B) \and (B \iff C) \imp (B \imp A) \imp C \imp A
23 iff_decompbwd 
(A \iff B) \imp B \imp A
24 23 _hyp_null_complete 
(A \iff B) \and (B \iff C) \imp (A \iff B) \imp B \imp A
25 24, 8 _hyp_mp 
(A \iff B) \and (B \iff C) \imp B \imp A
26 22, 25 _hyp_mp 
(A \iff B) \and (B \iff C) \imp C \imp A
27 16, 26 _hyp_mp 
(A \iff B) \and (B \iff C) \imp (A \iff C)
28 27 _hyp_rm 
(A \iff B) \imp (B \iff C) \imp (A \iff C)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)