©1992-2000 Colin Allen. Reproduction by any means strictly prohibited.

The text book says:
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