And Elimination is a rule of inference that allows us to derive conjuncts from a conjunction. If a proof contains the conjunction of φ1 through φn, then we can deduce any of the conjuncts.