\iff同时引入\imp
theorem iff_simintro_imp (A B C D: wff): $ (A \iff B) \imp (C \iff D) \imp (A \imp C \iff B \imp D) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_comp | ((A \imp C) \imp B \imp D) \imp ((B \imp D) \imp A \imp C) \imp (A \imp C \iff B \imp D) |
|
| 2 | 1 | _hyp_null_complete | (A \iff B) \and (C \iff D) \imp ((A \imp C) \imp B \imp D) \imp ((B \imp D) \imp A \imp C) \imp (A \imp C \iff B \imp D) |
| 3 | imp_tran | (B \imp C) \imp (C \imp D) \imp B \imp D |
|
| 4 | 3 | _hyp_null_complete | (A \iff B) \and (C \iff D) \and (A \imp C) \imp (B \imp C) \imp (C \imp D) \imp B \imp D |
| 5 | imp_tran | (B \imp A) \imp (A \imp C) \imp B \imp C |
|
| 6 | 5 | _hyp_null_complete | (A \iff B) \and (C \iff D) \and (A \imp C) \imp (B \imp A) \imp (A \imp C) \imp B \imp C |
| 7 | iff_decompbwd | (A \iff B) \imp B \imp A |
|
| 8 | 7 | _hyp_null_complete | (A \iff B) \and (C \iff D) \imp (A \iff B) \imp B \imp A |
| 9 | _hyp_null_intro | (A \iff B) \imp (A \iff B) |
|
| 10 | 9 | _hyp_complete | (A \iff B) \and (C \iff D) \imp (A \iff B) |
| 11 | 8, 10 | _hyp_mp | (A \iff B) \and (C \iff D) \imp B \imp A |
| 12 | 11 | _hyp_complete | (A \iff B) \and (C \iff D) \and (A \imp C) \imp B \imp A |
| 13 | 6, 12 | _hyp_mp | (A \iff B) \and (C \iff D) \and (A \imp C) \imp (A \imp C) \imp B \imp C |
| 14 | _hyp_intro | (A \iff B) \and (C \iff D) \and (A \imp C) \imp A \imp C |
|
| 15 | 13, 14 | _hyp_mp | (A \iff B) \and (C \iff D) \and (A \imp C) \imp B \imp C |
| 16 | 4, 15 | _hyp_mp | (A \iff B) \and (C \iff D) \and (A \imp C) \imp (C \imp D) \imp B \imp D |
| 17 | iff_decomp | (C \iff D) \imp C \imp D |
|
| 18 | 17 | _hyp_null_complete | (A \iff B) \and (C \iff D) \imp (C \iff D) \imp C \imp D |
| 19 | _hyp_intro | (A \iff B) \and (C \iff D) \imp (C \iff D) |
|
| 20 | 18, 19 | _hyp_mp | (A \iff B) \and (C \iff D) \imp C \imp D |
| 21 | 20 | _hyp_complete | (A \iff B) \and (C \iff D) \and (A \imp C) \imp C \imp D |
| 22 | 16, 21 | _hyp_mp | (A \iff B) \and (C \iff D) \and (A \imp C) \imp B \imp D |
| 23 | 22 | _hyp_rm | (A \iff B) \and (C \iff D) \imp (A \imp C) \imp B \imp D |
| 24 | 2, 23 | _hyp_mp | (A \iff B) \and (C \iff D) \imp ((B \imp D) \imp A \imp C) \imp (A \imp C \iff B \imp D) |
| 25 | imp_tran | (A \imp D) \imp (D \imp C) \imp A \imp C |
|
| 26 | 25 | _hyp_null_complete | (A \iff B) \and (C \iff D) \and (B \imp D) \imp (A \imp D) \imp (D \imp C) \imp A \imp C |
| 27 | imp_tran | (A \imp B) \imp (B \imp D) \imp A \imp D |
|
| 28 | 27 | _hyp_null_complete | (A \iff B) \and (C \iff D) \and (B \imp D) \imp (A \imp B) \imp (B \imp D) \imp A \imp D |
| 29 | iff_decomp | (A \iff B) \imp A \imp B |
|
| 30 | 29 | _hyp_null_complete | (A \iff B) \and (C \iff D) \imp (A \iff B) \imp A \imp B |
| 31 | 30, 10 | _hyp_mp | (A \iff B) \and (C \iff D) \imp A \imp B |
| 32 | 31 | _hyp_complete | (A \iff B) \and (C \iff D) \and (B \imp D) \imp A \imp B |
| 33 | 28, 32 | _hyp_mp | (A \iff B) \and (C \iff D) \and (B \imp D) \imp (B \imp D) \imp A \imp D |
| 34 | _hyp_intro | (A \iff B) \and (C \iff D) \and (B \imp D) \imp B \imp D |
|
| 35 | 33, 34 | _hyp_mp | (A \iff B) \and (C \iff D) \and (B \imp D) \imp A \imp D |
| 36 | 26, 35 | _hyp_mp | (A \iff B) \and (C \iff D) \and (B \imp D) \imp (D \imp C) \imp A \imp C |
| 37 | iff_decompbwd | (C \iff D) \imp D \imp C |
|
| 38 | 37 | _hyp_null_complete | (A \iff B) \and (C \iff D) \imp (C \iff D) \imp D \imp C |
| 39 | 38, 19 | _hyp_mp | (A \iff B) \and (C \iff D) \imp D \imp C |
| 40 | 39 | _hyp_complete | (A \iff B) \and (C \iff D) \and (B \imp D) \imp D \imp C |
| 41 | 36, 40 | _hyp_mp | (A \iff B) \and (C \iff D) \and (B \imp D) \imp A \imp C |
| 42 | 41 | _hyp_rm | (A \iff B) \and (C \iff D) \imp (B \imp D) \imp A \imp C |
| 43 | 24, 42 | _hyp_mp | (A \iff B) \and (C \iff D) \imp (A \imp C \iff B \imp D) |
| 44 | 43 | _hyp_rm | (A \iff B) \imp (C \iff D) \imp (A \imp C \iff B \imp D) |