Rule of Distribution/Conjunction Distributes over Disjunction/Right Distributive/Formulation 2

Theorem

The conjunction operator is right distributive over the disjunction operator:

$\vdash \paren {\paren {q \lor r} \land p} \iff \paren {\paren {q \land p} \lor \paren {r \land p} }$

Proof

By the tableau method of natural deduction:

$\vdash \paren {\paren {q \lor r} \land p} \iff \paren {\paren {q \land p} \lor \paren {r \land p} } $

Line		Pool	Formula	Rule	Depends upon	Notes
1		1	$\paren {q \lor r} \land p$	Assumption	(None)
2		1	$\paren {q \land p} \lor \paren {r \land p}$	Sequent Introduction	1	Conjunction is Right Distributive over Disjunction: Formulation 1
3			$\paren {\paren {q \lor r} \land p} \implies \paren {\paren {q \land p} \lor \paren {r \land p} }$	Rule of Implication: $\implies \II$	1 – 2	Assumption 1 has been discharged
4		4	$\paren {q \land p} \lor \paren {r \land p}$	Assumption	(None)
5		4	$\paren {q \lor r} \land p$	Sequent Introduction	4	Conjunction is Right Distributive over Disjunction: Formulation 1
6			$\paren {\paren {q \land p} \lor \paren {r \land p} } \implies \paren {\paren {q \lor r} \land p}$	Rule of Implication: $\implies \II$	4 – 5	Assumption 4 has been discharged
7			$\paren {\paren {q \lor r} \land p} \iff \paren {\paren {q \land p} \lor \paren {r \land p} }$	Biconditional Introduction: $\iff \II$	3, 6

{{qed}