Rule bij_eliml

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

Bijunction elimination to obtain the left subjunction.