| double-arrow- elim |
Given a biconditional sentence Φ ↔Ψ (at line m), conclude either Φ → Ψ orΨ→Φ. |
| Annotation: m ↔E | |
| Assumption set: the same as at m. | |
| Also known as: Sometimes the rules ↔I and ↔E are subsumed as Definition of Biconditional (df.↔). | |
| Examples. | |
1 (1) P ↔ Q A | |
1 (2) P→Q 1 ↔E | |
| or | 1 (2) Q → P 1 ↔E |