| double-arrow- intro | Given two conditional sentences having the forms Φ → Ψ and Ψ→Φ (at lines m and n), conclude a biconditional with Φ on one side and Ψ on the other. |
| Annotation: m, n ↔I | |
| Assumption set:The union of the assumption sets at lines m and n. | |
| Comment: The order of m and n in the proof is irrelevant. | |
| Examples. | |
1 (1) P→Q A | |
2 (2) Q→P A | |
1,2 (3) P↔ Q 1,2 ↔I | |
| or | 1,2 (3) Q ↔ P 1,2 ↔I |