Theorem lsubj_elim
Theorem.
lsubj_elim
(A ↔ B) → A → B
Proof
01. 1 ⊢ A ↔ B,
hypo
. 02. 1 ⊢ A → B,
bij_eliml
1. lsubj_elim. ⊢ (A ↔ B) → A → B,
subj_intro
2.