\iff同时引入\iff
theorem iff_simintro_iff (A B C D: wff): $ (A \iff B) \imp (C \iff D) \imp ((A \iff C) \iff B \iff D) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_simintro_and | (A \imp C \iff B \imp D) \imp (C \imp A \iff D \imp B) \imp ((A \imp C) \and (C \imp A) \iff (B \imp D) \and (D \imp B)) |
|
| 2 | 1 | _hyp_null_complete | (A \iff B) \and (C \iff D) \imp (A \imp C \iff B \imp D) \imp (C \imp A \iff D \imp B) \imp ((A \imp C) \and (C \imp A) \iff (B \imp D) \and (D \imp B)) |
| 3 | iff_simintro_imp | (A \iff B) \imp (C \iff D) \imp (A \imp C \iff B \imp D) |
|
| 4 | 3 | _hyp_null_complete | (A \iff B) \and (C \iff D) \imp (A \iff B) \imp (C \iff D) \imp (A \imp C \iff B \imp D) |
| 5 | _hyp_null_intro | (A \iff B) \imp (A \iff B) |
|
| 6 | 5 | _hyp_complete | (A \iff B) \and (C \iff D) \imp (A \iff B) |
| 7 | 4, 6 | _hyp_mp | (A \iff B) \and (C \iff D) \imp (C \iff D) \imp (A \imp C \iff B \imp D) |
| 8 | _hyp_intro | (A \iff B) \and (C \iff D) \imp (C \iff D) |
|
| 9 | 7, 8 | _hyp_mp | (A \iff B) \and (C \iff D) \imp (A \imp C \iff B \imp D) |
| 10 | 2, 9 | _hyp_mp | (A \iff B) \and (C \iff D) \imp (C \imp A \iff D \imp B) \imp ((A \imp C) \and (C \imp A) \iff (B \imp D) \and (D \imp B)) |
| 11 | iff_simintro_imp | (C \iff D) \imp (A \iff B) \imp (C \imp A \iff D \imp B) |
|
| 12 | 11 | _hyp_null_complete | (A \iff B) \and (C \iff D) \imp (C \iff D) \imp (A \iff B) \imp (C \imp A \iff D \imp B) |
| 13 | 12, 8 | _hyp_mp | (A \iff B) \and (C \iff D) \imp (A \iff B) \imp (C \imp A \iff D \imp B) |
| 14 | 13, 6 | _hyp_mp | (A \iff B) \and (C \iff D) \imp (C \imp A \iff D \imp B) |
| 15 | 10, 14 | _hyp_mp | (A \iff B) \and (C \iff D) \imp ((A \imp C) \and (C \imp A) \iff (B \imp D) \and (D \imp B)) |
| 16 | 15 | conv iff | (A \iff B) \and (C \iff D) \imp ((A \iff C) \iff B \iff D) |
| 17 | 16 | _hyp_rm | (A \iff B) \imp (C \iff D) \imp ((A \iff C) \iff B \iff D) |