\iff交换
theorem iff_comm (A B: wff): $ (A \iff B) \iff B \iff A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_comp | ((A \iff B) \imp (B \iff A)) \imp ((B \iff A) \imp (A \iff B)) \imp ((A \iff B) \iff B \iff A) |
|
| 2 | iff_symm | (A \iff B) \imp (B \iff A) |
|
| 3 | 1, 2 | ax_mp | ((B \iff A) \imp (A \iff B)) \imp ((A \iff B) \iff B \iff A) |
| 4 | iff_symm | (B \iff A) \imp (A \iff B) |
|
| 5 | 3, 4 | ax_mp | (A \iff B) \iff B \iff A |