Theorem iff_imp_insl ≪ | index | src | ≫

\iff\imp左插入

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)