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: 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 "

The conjunction elimination sub-rules may be written in sequent notation: and where

in logical system; and expressed as truth-functional tautologies or theorems of propositional logic: and where

are propositions expressed in some formal system.