title: Conjunction elimination
text: # Conjunction elimination
  
  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:
  
      ${\frac {P\land Q}{\therefore P}}$
  
  and
  
      ${\frac {P\land Q}{\therefore Q}}$
  
  The two sub-rules together mean that, whenever an instance of "$P\land Q$" appears on a line of a proof, either "$P$" or "$Q$" 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:
  
      $(P\land Q)\vdash P$
  
  and
  
      $(P\land Q)\vdash Q$
  
  where $\vdash$ is a metalogical symbol meaning that $P$ is a syntactic consequence of $P\land Q$ and $Q$ is also a syntactic consequence of $P\land Q$ in logical system;
  
  and expressed as truth-functional tautologies or theorems of propositional logic:
  
      $(P\land Q)\to P$
  
  and
  
      $(P\land Q)\to Q$
  
  where $P$ and $Q$ are propositions expressed in some formal system.
  
  