\iff右引入\iff
theorem iff_intror_iff (A B C: wff): $ (A \iff B) \imp ((A \iff C) \iff B \iff C) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_imp_elimrsl | ((A \iff B) \imp (C \iff C) \imp ((A \iff C) \iff B \iff C)) \imp (C \iff C) \imp (A \iff B) \imp ((A \iff C) \iff B \iff C) |
|
| 2 | iff_simintro_iff | (A \iff B) \imp (C \iff C) \imp ((A \iff C) \iff B \iff C) |
|
| 3 | 1, 2 | ax_mp | (C \iff C) \imp (A \iff B) \imp ((A \iff C) \iff B \iff C) |
| 4 | iff_refl | C \iff C |
|
| 5 | 3, 4 | ax_mp | (A \iff B) \imp ((A \iff C) \iff B \iff C) |