Constructive Dilemma/Formulation 3

From ProofWiki
Jump to navigation Jump to search

Theorem

$\left({p \implies q}\right) \land \left({r \implies s}\right), p \lor r \vdash q \lor s$


Proof

By the tableau method of natural deduction:

$\left({p \implies q}\right) \land \left({r \implies s}\right), p \lor r \vdash q \lor s$
Line Pool Formula Rule Depends upon Notes
1 1 $\left({p \implies q}\right) \land \left({r \implies s}\right)$ Premise (None)
2 2 $p \lor r$ Premise (None)
3 1, 2 $\left({p \lor r}\right) \land \left({p \implies q}\right) \land \left({r \implies s}\right)$ Rule of Conjunction: $\land \mathcal I$ 2, 1 Associativity is implicit
4 $\left({\left({p \lor r}\right) \land \left({p \implies q}\right) \land \left({r \implies s}\right)}\right) \implies \left({q \lor s}\right)$ Theorem Introduction (None) Constructive Dilemma: Formulation 2
5 1, 2 $q \lor s$ Modus Ponendo Ponens: $\implies \mathcal E$ 4, 3

$\blacksquare$


Sources