Definition
Elimination Inference Rule
An elimination inference rule is an inference rule that specifies how to use a formula according to its outermost logical connective or quantifier to derive a consequence. Depending on the calculus, it may be primitive or derived; the name describes its role, not its status.
For conjunction in natural deduction: