Factor Principles/Disjunction on Right/Formulation 1/Proof 3

From ProofWiki
Jump to navigation Jump to search

Theorem

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


Proof

By the tableau method of natural deduction:

$p \implies q \vdash \paren {p \lor r} \implies \paren {q \lor r} $
Line Pool Formula Rule Depends upon Notes
1 1 $p \implies q$ Premise (None)
2 2 $p \lor r$ Assumption (None)
3 2 $r \lor p$ Sequent Introduction 2 Disjunction is Commutative
4 1 $\paren {r \lor p} \implies \paren {r \lor q}$ Sequent Introduction 1 Factor Principles/Disjunction on Left/Formulation 1
5 1,2 $r \lor q$ Modus Ponendo Ponens: $\implies \mathcal E$ 4, 3
6 1,2 $q \lor r$ Sequent Introduction 5 Disjunction is Commutative
7 1 $\paren {p \lor r} \implies \paren {q \lor r}$ Rule of Implication: $\implies \II$ 2 – 6 Assumption 2 has been discharged

$\blacksquare$