Theorem imp_iff_extl ≪ | index | src | ≫

\imp\iff左提取

theorem imp_iff_extl (A B C: wff):
  $ (A \imp B \iff A \imp C) \imp A \imp (B \iff C) $;
StepHypRefExpression
1 imp_and_extl 
(A \imp B \imp C) \and (A \imp C \imp B) \imp A \imp (B \imp C) \and (C \imp B)
2 1 _hyp_null_complete 
(A \imp B \iff A \imp C) \imp (A \imp B \imp C) \and (A \imp C \imp B) \imp A \imp (B \imp C) \and (C \imp B)
3 and_comp 
(A \imp B \imp C) \imp (A \imp C \imp B) \imp (A \imp B \imp C) \and (A \imp C \imp B)
4 3 _hyp_null_complete 
(A \imp B \iff A \imp C) \imp (A \imp B \imp C) \imp (A \imp C \imp B) \imp (A \imp B \imp C) \and (A \imp C \imp B)
5 imp_imp_extl 
((A \imp B) \imp A \imp C) \imp A \imp B \imp C
6 5 _hyp_null_complete 
(A \imp B \iff A \imp C) \imp ((A \imp B) \imp A \imp C) \imp A \imp B \imp C
7 iff_decomp 
(A \imp B \iff A \imp C) \imp (A \imp B) \imp A \imp C
8 7 _hyp_null_complete 
(A \imp B \iff A \imp C) \imp (A \imp B \iff A \imp C) \imp (A \imp B) \imp A \imp C
9 _hyp_null_intro 
(A \imp B \iff A \imp C) \imp (A \imp B \iff A \imp C)
10 8, 9 _hyp_mp 
(A \imp B \iff A \imp C) \imp (A \imp B) \imp A \imp C
11 6, 10 _hyp_mp 
(A \imp B \iff A \imp C) \imp A \imp B \imp C
12 4, 11 _hyp_mp 
(A \imp B \iff A \imp C) \imp (A \imp C \imp B) \imp (A \imp B \imp C) \and (A \imp C \imp B)
13 imp_imp_extl 
((A \imp C) \imp A \imp B) \imp A \imp C \imp B
14 13 _hyp_null_complete 
(A \imp B \iff A \imp C) \imp ((A \imp C) \imp A \imp B) \imp A \imp C \imp B
15 iff_decompbwd 
(A \imp B \iff A \imp C) \imp (A \imp C) \imp A \imp B
16 15 _hyp_null_complete 
(A \imp B \iff A \imp C) \imp (A \imp B \iff A \imp C) \imp (A \imp C) \imp A \imp B
17 16, 9 _hyp_mp 
(A \imp B \iff A \imp C) \imp (A \imp C) \imp A \imp B
18 14, 17 _hyp_mp 
(A \imp B \iff A \imp C) \imp A \imp C \imp B
19 12, 18 _hyp_mp 
(A \imp B \iff A \imp C) \imp (A \imp B \imp C) \and (A \imp C \imp B)
20 2, 19 _hyp_mp 
(A \imp B \iff A \imp C) \imp A \imp (B \imp C) \and (C \imp B)
21 20 conv iff 
(A \imp B \iff A \imp C) \imp A \imp (B \iff C)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)