In propositional logic, simplification^[1][2][3] (equivalent to conjunction elimination) 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:

${\displaystyle {\frac {P\lor Q}{\therefore P))}$

or as

${\displaystyle {\frac {P\lor Q}{\therefore Q))}$

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

The simplification rule may be written in sequent notation:

${\displaystyle (P\lor Q)\vdash P}$

or as

${\displaystyle (P\lor Q)\vdash Q}$

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

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

${\displaystyle (P\lor Q)\to P}$

and

${\displaystyle (P\lor Q)\to Q}$

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