\iff同时引入\or
theorem iff_simintro_or (A B C D: wff): $ (A \iff B) \imp (C \iff D) \imp (A \or C \iff B \or D) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_simintro_imp | (\neg A \iff \neg B) \imp (C \iff D) \imp (\neg A \imp C \iff \neg B \imp D) |
|
| 2 | 1 | _hyp_null_complete | (A \iff B) \and (C \iff D) \imp (\neg A \iff \neg B) \imp (C \iff D) \imp (\neg A \imp C \iff \neg B \imp D) |
| 3 | iff_intro_neg | (A \iff B) \imp (\neg A \iff \neg B) |
|
| 4 | 3 | _hyp_null_complete | (A \iff B) \and (C \iff D) \imp (A \iff B) \imp (\neg A \iff \neg B) |
| 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 (\neg A \iff \neg B) |
| 8 | 2, 7 | _hyp_mp | (A \iff B) \and (C \iff D) \imp (C \iff D) \imp (\neg A \imp C \iff \neg B \imp D) |
| 9 | _hyp_intro | (A \iff B) \and (C \iff D) \imp (C \iff D) |
|
| 10 | 8, 9 | _hyp_mp | (A \iff B) \and (C \iff D) \imp (\neg A \imp C \iff \neg B \imp D) |
| 11 | 10 | conv or | (A \iff B) \and (C \iff D) \imp (A \or C \iff B \or D) |
| 12 | 11 | _hyp_rm | (A \iff B) \imp (C \iff D) \imp (A \or C \iff B \or D) |