lsubj_conj

Theorem lsubj_conj_eliml

Theorem. lsubj_conj_eliml
(E ↔ A ∧ B) → E → A

Proof
01. 1 ⊢ E ↔ A ∧ B, hypo.
02. 2 ⊢ E, hypo.
03. 1, 2 ⊢ A ∧ B, lsubj_elim 1 2.
04. 1, 2 ⊢ A, conj_eliml 3.
lsubj_conj_eliml. ⊢ (E ↔ A ∧ B) → E → A, subj_intro_ii 4.