Theorem. lsubj_conj_elimllr
(E ↔ A ∧ B ∧ C ∧ D) → E → B
Proof
01. 1 ⊢ E ↔ A ∧ B ∧ C ∧ D, hypo.
02. 2 ⊢ E, hypo.
03. 1, 2 ⊢ A ∧ B ∧ C ∧ D, lsubj_elim 1 2.
04. 1, 2 ⊢ B, conj_elimllr 3.
lsubj_conj_elimllr. ⊢ (E ↔ A ∧ B ∧ C ∧ D) → E → B, subj_intro_ii 4.