Conjunction elimination

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:

${\displaystyle \frac{P\wedge Q}{\therefore P}}$

and

${\displaystyle \frac{P\wedge Q}{\therefore Q}}$

The two sub-rules together mean that, whenever an instance of "${\displaystyle P\wedge Q}$" appears on a line of a proof, either "${\displaystyle P}$" or "${\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:

${\displaystyle (P\wedge Q)⊢P}$

and

${\displaystyle (P\wedge Q)⊢Q}$

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

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

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

and

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

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