Conjunction elimination
Transformation rules 

Propositional calculus 
Rules of inference 
Rules of replacement 

Predicate logic 
In propositional logic, conjunction elimination (also called and elimination, ∧ elimination,^{} or simplification)^{}^{}^{} 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 subrules, which can be expressed in formal language as:
and
The two subrules 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 subrule.
Formal notation
The conjunction elimination subrules may be written in sequent notation:
and
where is a metalogical symbol meaning that is a syntactic consequence of and is also a syntactic consequence of in logical system;
and expressed as truthfunctional tautologies or theorems of propositional logic:
and
where and are propositions expressed in some formal system.