Theorem: Rule of Association/Disjunction/Formulation 2/Forward Implication

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

Proof:
{{BeginTableau|\vdash \paren {p \lor \paren {q \lor r} } \implies \paren {\paren {p \lor q} \lor r}|Instance 2 of the Hilbert-style systems}}
{{TableauLine
 | n = 1
 | f = \paren {\paren {p \lor q} \lor r} \implies \paren {p \lor \paren {q \lor r} }
 | rlnk = Rule of Association/Disjunction/Formulation 2/Reverse Implication
 | rtxt = Rule of Association: Reverse Implication
}}
{{TableauLine
 | n = 2
 | f = \paren {q \lor r} \implies \paren {r \lor q}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 3$
 | c = $q \,/\, p, r \,/\, q$
}}
{{TableauLine
 | n = 3
 | f = \paren {\paren {q \lor r} \implies \paren {r \lor q} } \implies \paren {\paren {p \lor \paren {q \lor r} } \implies \paren {p \lor \paren {r \lor q} } }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 4$
 | c = $\paren {q \lor r} \,/\, q, \paren {r \lor q} \,/\, r$
}}
{{TableauLine
 | n = 4
 | f = \paren {p \lor \paren {q \lor r} } \implies \paren {p \lor \paren {r \lor q} }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 3$
 | dep  = 2, 3
}}
{{TableauLine
 | n = 5
 | f = \paren {\paren {p \lor q} \lor r} \implies \paren {p \lor \paren {r \lor q} }
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep  = 1, 4
}}
{{TableauLine
 | n = 6
 | f = \paren {p \lor \paren {r \lor q} } \implies \paren {\paren {r \lor q} \lor p}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 3$
 | c = $\paren {r \lor q} \,/\, q$
}}
{{TableauLine
 | n = 7
 | f = \paren {\paren {p \lor q} \lor r} \implies \paren {\paren {r \lor q} \lor p}
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep  = 5, 6
}}
{{TableauLine
 | n = 8
 | f = \paren {r \lor \paren {p \lor q} } \implies \paren {\paren {p \lor q} \lor r}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 3$
 | c = $r \,/\, p, \paren {p \lor q} \,/\, q$
}}
{{TableauLine
 | n = 9
 | f = \paren {r \lor \paren {p \lor q} } \implies \paren {\paren {r \lor q} \lor p}
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep  = 7, 8
}}
{{TableauLine
 | n = 10
 | f = \paren {q \lor p} \implies \paren {p \lor q}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 3$
 | c = $p / q, q / p$
}}
{{TableauLine
 | n = 11
 | f = \paren {\paren {q \lor p} \implies \paren {p \lor q} } \implies \paren {\paren {r \lor \paren {q \lor p} } \implies \paren {r \lor \paren {p \lor q} } }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 4$
 | c = $r \,/\, p, \paren {q \lor p} \,/\, q, \paren {p \lor q} \,/\, r$
}}
{{TableauLine
 | n = 12
 | f = \paren {r \lor \paren {q \lor p} } \implies \paren {r \lor \paren {p \lor q} }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 3$
 | dep  = 10, 11
}}
{{TableauLine
 | n = 13
 | f = \paren {r \lor \paren {q \lor p} } \implies \paren {\paren {r \lor q} \lor p}
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep  = 9, 12
}}
{{TableauLine
 | n = 14
 | f = \paren {p \lor \paren {q \lor r} } \implies \paren {\paren {p \lor q} \lor r}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 1$
 | dep = 13
 | c = $r / p, p / r$
}}
{{EndTableau}}
{{qed}}