Rule conj_eliml

Rule. conj_eliml
(H ⊢ A ∧ B) → (H ⊢ A)

Conjunction elimination to obtain the left proposition.