Conjunction elimination rule (source code)

= Conjunction elimination rule

= Conjunction elimination
{synonym}

The <conjunction elimination rule> in <natural deduction> permits both inferences
$$
\frac{A\land B}{A},\qquad \frac{A\land B}{B}.
$$
The symbol $\land$ denotes <logical conjunction>. A proof of the conjunction supplies each of its component <propositions>, so either component can be used in a later argument.

For example, from $0<x\land x<1$ one can infer $0<x$ when establishing positivity, and separately infer $x<1$ when establishing an upper bound. The <truth table> makes the rule sound: every assignment satisfying the conjunction satisfies both components.