Conjunction elimination

Transformation rules
Propositional calculus
Rules of inference
Modus ponens / Modus tollens Biconditional introduction / elimination Conjunction introduction / elimination Disjunction introduction / elimination Disjunctive / Hypothetical syllogism Constructive / Destructive dilemma Absorption Modus ponendo tollens
Rules of replacement
Associativity Commutativity Distributivity Double negation De Morgan's laws Transposition Material implication Exportation Tautology Negation introduction
Predicate logic
Universal generalization / instantiation Existential generalization / instantiation

In propositional logic, conjunction elimination (also called and elimination, ∧ elimination,^[1] or simplification)^[2]^[3]^[4] is a valid immediate inference, argument form and rule of inference which makes the inference that, if the conjunction A and B is true, then A is true, and B is true. The rule makes it possible to shorten longer proofs by deriving one of the conjuncts of a conjunction on a line by itself.

An example in English:

It's raining and it's pouring.

Therefore it's raining.

The rule can be expressed in formal language as:

\frac{P \land Q}{\therefore P}

or as

\frac{P \land Q}{\therefore Q}

where the rule is that whenever instances of " $P \land Q$ " appear on lines of a proof, either " $P$ " or " $Q$ " can be placed on a subsequent line by itself.

Formal notation

The conjunction elimination rule may be written in sequent notation:

(P \land Q) \vdash P

or as

(P \land Q) \vdash Q

where $\vdash$ is a metalogical symbol meaning that $P$ is a syntactic consequence of $P \land Q$ and $Q$ is also a syntactic consequence of $P \land Q$ in logical system;

and expressed as a truth-functional tautology or theorem of propositional logic:

(P \land Q) \to P

and

(P \land Q) \to Q

where $P$ and $Q$ are propositions expressed in some formal system.

References

↑ David A. Duffy (1991). Principles of Automated Theorem Proving. New York: Wiley. Sect.3.1.2.1, p.46
↑ Copi and Cohen
↑ Moore and Parker
↑ Hurley