Theorem: Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive

==== Formulation 1 ====
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 2}}

Proof:
{{BeginTableau|\vdash \paren {p \lor \paren {q \land r} } \implies \paren {\paren {p \lor q} \land \paren {p \lor r} }|Instance 2 of the Hilbert-style systems}}
{{TableauLine
 | n = 1
 | f = \paren {q \land r} \implies q
 | rlnk = Rule of Simplification/Sequent Form/Formulation 2/Form 1
 | rtxt = Rule of Simplification
 | c = $q / p, r / q$
}}
{{TableauLine
 | n = 2
 | f = \paren {\paren {q \land r} \implies q} \implies \paren {\paren {p \lor \paren {q \land r} } \implies \paren {p \lor q} }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $A 4$
 | c = $\paren {q \land r} \, / \, q, q \, / \, r$
}}
{{TableauLine
 | n = 3
 | f = \paren {p \lor \paren {q \land r} } \implies \paren {p \lor q}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $RST \, 3$
 | dep = 1, 2
}}
{{TableauLine
 | n = 4
 | f = \paren {q \land r} \implies \paren {r \land q}
 | rlnk = Rule of Commutation/Conjunction/Formulation 2
 | rtxt = Rule of Commutation
 | c = $q / p, r / q$
}}
{{TableauLine
 | n = 5
 | f = \paren {r \land q} \implies r
 | rlnk = Rule of Simplification/Sequent Form/Formulation 2/Form 1
 | rtxt = Rule of Simplification
 | c = $r / p$
}}
{{TableauLine
 | n = 6
 | f = \paren {q \land r} \implies r
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep = 4, 5
}}
{{TableauLine
 | n = 7
 | f = \paren {\paren {q \land r} \implies r} \implies \paren {\paren {p \lor \paren {q \land r} } \implies \paren {p \lor r} }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $A4$
 | c = $\paren {q \land r} \, / \, q$
}}
{{TableauLine
 | n = 8
 | f = \paren {p \lor \paren {q \land r} } \implies \paren {p \lor r}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $RST \, 3$
 | dep = 6, 7
}}
{{TableauLine
 | n = 9
 | f = \paren {p \lor q} \implies \paren {\paren {p \lor r} \implies \paren {\paren {p \lor q} \land \paren {p \lor r} } }
 | rlnk = Rule of Conjunction/Sequent Form/Formulation 2
 | rtxt = Rule of Conjunction
 | c = $\paren {p \lor q} \, / \, p, \paren {p \lor r} \, / \, q$
}}
{{TableauLine
 | n = 10
 | f = \paren {p \lor \paren {q \land r} } \implies \paren {\paren {p \lor r} \implies \paren {\paren {p \lor q} \land \paren {p \lor r} } }
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep = 3, 9
}}
{{TableauLine
 | n = 11
 | f = \paren {\paren {p \lor \paren {q \land r} } \implies \paren {\paren {p \lor r} \implies \paren {p \lor q} \land \paren {p \lor r} } } \\ \implies \paren {\paren {p \lor r} \implies \paren {\paren {p \lor \paren {q \land r} } \implies \paren {p \lor q} \land \paren {p \lor r} } }
 | rlnk = Principle of Commutation/Formulation 2/Forward Implication
 | rtxt = Principle of Commutation
 | c = $\paren {p \lor \paren {q \land r} } \, / \, p, \paren {p \lor r} \, / \, q, \paren {\paren {p \lor q} \land \paren {p \lor r} } \, / \, r$
}}
{{TableauLine
 | n = 12
 | f = \paren {p \lor r} \implies \paren {\paren {p \lor \paren {q \land r} } \implies \paren {p \lor q} \land \paren {p \lor r} }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $RST \, 3$
 | dep = 10, 11
}}
{{TableauLine
 | n = 13
 | f = \paren {p \lor \paren {q \land r} } \implies \paren {\paren {p \lor \paren {q \land r} } \implies \paren {p \lor q} \land \paren {p \lor r} }
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep = 8, 12
}}
{{TableauLine
 | n = 14
 | f = \paren {p \lor \paren {q \land r} } \implies \paren {p \lor q} \land \paren {p \lor r}
}}
{{EndTableau}}
{{Qed}}