Conjunction elimination (source code)

= Conjunction elimination
{wiki=Conjunction_elimination}

Conjunction elimination is a rule of inference in propositional logic that allows one to derive a single component of a conjunction from the conjunction itself. The rule can be formally stated as follows: If you have a conjunction \\( P \\land Q \\) (where \\( P \\) and \\( Q \\) are any propositions), you can infer each of its components separately: 1. From \\( P \\land Q \\), infer \\( P \\).