Rule. bij_eliml
(H ⊢ A ↔ B) → (H ⊢ A → B)