Disjunction elimination

<h2 id="formal-notation">Formal notation</h2>
<p>The <i>disjunction elimination</i> rule may be written in <a href="/facts/Sequent/7YoB2hYb">sequent</a> notation:
</p>

(
        P
        →
        Q
        )
        ,
        (
        R
        →
        Q
        )
        ,
        (
        P
        ∨
        R
        )
        ⊢
        Q
      
    
    {\displaystyle (P\to Q),(R\to Q),(P\lor R)\vdash Q}

<p>where 
  
    
      
        ⊢
      
    
    {\displaystyle \vdash }
  
 is a <a href="/facts/Metalogic/zfooQjCo">metalogical</a> symbol meaning that 
  
    
      
        Q
      
    
    {\displaystyle Q}
  
 is a <a href="/facts/Logical_consequence/AyDXp4dn">syntactic consequence</a> of 
  
    
      
        P
        →
        Q
      
    
    {\displaystyle P\to Q}
  
, and 
  
    
      
        R
        →
        Q
      
    
    {\displaystyle R\to Q}
  
 and 
  
    
      
        P
        ∨
        R
      
    
    {\displaystyle P\lor R}
  
 in some logical system;
</p><p>and expressed as a truth-functional <a href="/facts/Tautology_(logic)/p82wWMaN">tautology</a> or theorem of propositional logic:
</p>

(
        (
        (
        P
        →
        Q
        )
        ∧
        (
        R
        →
        Q
        )
        )
        ∧
        (
        P
        ∨
        R
        )
        )
        →
        Q
      
    
    {\displaystyle (((P\to Q)\land (R\to Q))\land (P\lor R))\to Q}

<p>where 
  
    
      
        P
      
    
    {\displaystyle P}
  
, 
  
    
      
        Q
      
    
    {\displaystyle Q}
  
, and 
  
    
      
        R
      
    
    {\displaystyle R}
  
 are propositions expressed in some <a href="/facts/Formal_system/KaeDAjK7">formal system</a>.
</p>
<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Disjunction/jbI2EGlM">Disjunction</a></li>
<li><a href="/facts/Argument_in_the_alternative/wMclAd5x">Argument in the alternative</a></li>
<li><a href="/facts/Disjunct_normal_form/hsw2pRPu">Disjunct normal form</a></li>
<li><a href="/facts/Proof_by_exhaustion/bTuwLV7R">Proof by exhaustion</a></li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>"Rule of Or-Elimination - ProofWiki". Archived from the original on 2015-04-18. Retrieved 2015-04-09. <a href="https://web.archive.org/web/20150418093657/https://proofwiki.org/wiki/Rule_of_Or-Elimination" target="_blank">https://web.archive.org/web/20150418093657/https://proofwiki.org/wiki/Rule_of_Or-Elimination</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>"Proof by cases". Archived from the original on 2002-03-07. <a href="https://web.archive.org/web/20020307080240/http://www.cs.gsu.edu/~cscskp/Automata/proofs/node6.html" target="_blank">https://web.archive.org/web/20020307080240/http://www.cs.gsu.edu/~cscskp/Automata/proofs/node6.html</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
</ol>

Disjunction elimination open-in-new

Disjunction elimination