# Conjunction elimination

Type Rule of inference Propositional calculus If the conjunction $\displaystyle{ A }$ and $\displaystyle{ B }$ is true, then $\displaystyle{ A }$ is true, and $\displaystyle{ B }$ is true.

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 consists of two separate sub-rules, which can be expressed in formal language as:

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

and

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

The two sub-rules together mean that, whenever an instance of "$\displaystyle{ P \land 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 \land Q) \vdash P }$

and

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

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

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

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

and

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

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

## References

1. David A. Duffy (1991). Principles of Automated Theorem Proving. New York: Wiley.  Sect.3.1.2.1, p.46
2. Copi and Cohen[citation needed]
3. Moore and Parker[citation needed]
4. Hurley[citation needed]

sv:Matematiskt uttryck#Förenkling