Theorem imp_iff_insr ≪ | index | src | ≫

\imp\iff右插入

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)