# Conjunction elimination

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Conjunction_elimination
> Markdown URL: https://mediated.wiki/source/Conjunction_elimination.md
> Source: https://en.wikipedia.org/wiki/Conjunction_elimination
> Source revision: 1314850935
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

{{Short description|Inference  rule in logic}}
{{Infobox mathematical statement
| name = Conjunction elimination
| type = [Rule of inference](/source/Rule_of_inference)
| field = [Propositional calculus](/source/Propositional_calculus)
| statement = If the conjunction <math>A</math> and <math>B</math> is true, then <math>A</math> is true, and <math>B</math> is true.
| symbolic statement = 
# <math>\frac{P \land Q}{\therefore P}, \frac{P \land Q}{\therefore Q}</math>
# <math>(P \land Q) \vdash P, (P \land Q) \vdash Q</math>
# <math> (P \land Q) \to P,(P \land Q) \to Q</math>
| conjectured by =
| conjecture date =
| first stated by =
| first stated in =
| first proof by =
| first proof date =
| open problem =
| known cases =
| implied by =
| equivalent to =
| generalizations =
| consequences =
}}
{{Transformation rules}}

In [propositional logic](/source/propositional_calculus), '''conjunction elimination''' (also called '''''and''''' '''elimination''', '''∧ elimination''',<ref>{{cite book | author=David A. Duffy | title=Principles of Automated Theorem Proving | location=New York | publisher=Wiley | year=1991 }} Sect.3.1.2.1, p.46</ref> or '''simplification''')<ref>Copi and Cohen{{cn|reason=Without title, this is hardly a useful reference.|date=February 2014}}</ref><ref>Moore and Parker{{cn|date=February 2014}}</ref><ref>Hurley{{cn|date=February 2014}}</ref> is a [valid](/source/Validity_(logic)) [immediate inference](/source/immediate_inference), [argument form](/source/argument_form) and [rule of inference](/source/rule_of_inference) which makes the [inference](/source/inference) that, if the [conjunction](/source/Logical_conjunction) ''A and B'' is true, then ''A'' is true, and ''B'' is true. The rule makes it possible to shorten longer [proofs](/source/formal_proof) by deriving one of the conjuncts of a conjunction on a line by itself. 

An example in [English](/source/English_language):
: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](/source/formal_language) as:

:<math>\frac{P \land Q}{\therefore P}</math>

and

:<math>\frac{P \land Q}{\therefore Q}</math>

The two sub-rules together mean that, whenever an instance of "<math>P \land Q</math>" appears on a line of a proof, either "<math>P</math>" or "<math>Q</math>" 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](/source/sequent) notation:

: <math>(P \land Q) \vdash P</math>
and
: <math>(P \land Q) \vdash Q</math>

where <math>\vdash</math> is a [metalogic](/source/metalogic)al symbol meaning that <math>P</math> is a [syntactic consequence](/source/logical_consequence) of <math>P \land Q</math> and <math>Q</math> is also a syntactic consequence of <math>P \land Q</math> in [logical system](/source/formal_system);

and expressed as truth-functional [tautologies](/source/tautology_(logic)) or [theorems](/source/theorems) of propositional logic:

:<math>(P \land Q) \to P</math>
and
:<math>(P \land Q) \to Q</math>

where <math>P</math> and <math>Q</math> are propositions expressed in some [formal system](/source/formal_system).

== References ==
{{reflist}}
{{logic-stub}}
Category:Rules of inference
Category:Theorems in propositional logic

[sv:Matematiskt uttryck#Förenkling](/source/sv%3AMatematiskt_uttryck)

---
Adapted from the Wikipedia article [Conjunction elimination](https://en.wikipedia.org/wiki/Conjunction_elimination) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Conjunction_elimination?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.