In propositional logic, conjunction elimination (also called and elimination, ∧ elimination, or simplification) 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 consists of two separate sub-rules, which can be expressed in formal language as:

P ∧ Q ∴ P {\displaystyle {\frac {P\land Q}{\therefore P}}}

and

P ∧ Q ∴ Q {\displaystyle {\frac {P\land Q}{\therefore Q}}}

The two sub-rules together mean that, whenever an instance of "P ∧ Q {\displaystyle P\land Q}" appears on a line of a proof, either "P {\displaystyle P}" or "Q {\displaystyle Q}" can be placed on a subsequent line by itself. The above example in English is an application of the first sub-rule.

Formal notation

The conjunction elimination sub-rules may be written in sequent notation:

( P ∧ Q ) ⊢ P {\displaystyle (P\land Q)\vdash P}

and

( P ∧ Q ) ⊢ Q {\displaystyle (P\land Q)\vdash Q}

where ⊢ {\displaystyle \vdash } is a metalogical symbol meaning that P {\displaystyle P} is a syntactic consequence of P ∧ Q {\displaystyle P\land Q} and Q {\displaystyle Q} is also a syntactic consequence of P ∧ Q {\displaystyle P\land Q} in logical system;

and expressed as truth-functional tautologies or theorems of propositional logic:

( P ∧ Q ) → P {\displaystyle (P\land Q)\to P}

and

( P ∧ Q ) → Q {\displaystyle (P\land Q)\to Q}

where P {\displaystyle P} and Q {\displaystyle Q} are propositions expressed in some formal system.