Proof 01. 1 ⊢ A ∧ (B ∧ C), hypo. 02. 1 ⊢ B ∧ C, conj_elimr 1. 03. 1 ⊢ B, conj_eliml 2. conj_elimrl. ⊢ A ∧ (B ∧ C) → B, subj_intro 3.