Conjunction elimination

Conjunction elimination
TypeRule of inference
FieldPropositional calculus
StatementIf the conjunction and is true, then is true, and is true.
Symbolic statement

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:

and

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

  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]