Factor Principles/Disjunction on Left/Formulation 1/Proof 1

From ProofWiki
Jump to navigation Jump to search

Theorem

$p \implies q \vdash \paren {r \lor p} \implies \paren {r \lor q}$


Proof

By the tableau method of natural deduction:

$p \implies q \vdash \paren {r \lor p} \implies \paren {r \lor q} $
Line Pool Formula Rule Depends upon Notes
1 1 $p \implies q$ Premise (None)
2 $r \implies r$ Theorem Introduction (None) Law of Identity: Formulation 2
3 1 $\paren {r \lor p} \implies \paren {r \lor q}$ Sequent Introduction 2, 1 Constructive Dilemma

$\blacksquare$