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 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. Formal notation The conjunction elimination sub-rules 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 truth-functional tautologies or theorems of propositional logic: and where and are propositions expressed in some formal system. References Rules of inference Theorems in propositional logic sv:Matematiskt uttryck#Förenkling