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

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

Proof:
By definition of $\impliedby$, we prove:
:$\vdash \paren {\paren {p \lor q} \lor r} \implies \paren {p \lor \paren {q \lor r} }$
{{BeginTableau|\vdash \paren {\paren {p \lor q} \lor r} \implies \paren {p \lor \paren {q \lor r} }|Instance 2 of the Hilbert-style systems}}
{{TableauLine
 | n = 1
 | f = r \implies \paren {q \lor r}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 2$
 | c = $r / q, q / p$
}}
{{TableauLine
 | n = 2
 | f = \paren {r \implies \paren {q \lor r} } \implies \paren {\paren {\paren {p \lor q} \lor r} \implies \paren {\paren {p \lor q} \lor \paren {q \lor r} } }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 4$
 | c = $r / q, \paren {p \lor q} \,/\, p, \paren {q \lor r} \,/\, r$
}}
{{TableauLine
 | n = 3
 | f = \paren {\paren {p \lor q} \lor r} \implies \paren {\paren {p \lor q} \lor \paren {q \lor r} }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 3$
 | dep  = 1, 2
}} <!-- D5 -->
{{TableauLine
 | n = 4
 | f = q \implies \paren {r \lor q}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 2$
 | c = $r / p$
}}
{{TableauLine
 | n = 5
 | f = \paren {q \implies \paren {r \lor q} } \implies \paren {\paren {p \lor q} \implies \paren {p \lor \paren {r \lor q} } }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 4$
 | c = $\paren {r \lor q} \,/\, r$
}}
{{TableauLine
 | n = 6
 | f = \paren {p \lor q} \implies \paren {p \lor \paren {r \lor q} }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 3$
 | dep  = 4, 5
}}
{{TableauLine
 | n = 7
 | 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 = 8
 | f = \paren {p \lor q} \implies \paren {\paren {r \lor q} \lor p}
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep  = 6, 7
}} <!-- D6 -->
{{TableauLine
 | n = 9
 | f = q \implies \paren {q \lor p}
 | rlnk = Rule of Addition/Sequent Form/Formulation 2/Form 1/Proof 2
 | rtxt = Rule of Addition
 | c = $p \,/\, q, q \,/\, p$
}}
{{TableauLine
 | n = 10
 | f = q \implies \paren {q \lor s}
 | rlnk = Rule of Addition/Sequent Form/Formulation 2/Form 1/Proof 2
 | rtxt = Rule of Addition
 | c = $s \,/\, q, q \,/\, p$
}}
{{TableauLine
 | n = 11
 | f = \paren {q \implies \paren {q \lor s} } \implies \paren {\paren {p \lor q} \implies \paren {p \lor \paren {q \lor s} } }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 4$
 | c = $\paren {q \lor s} \,/\, r$
}}
{{TableauLine
 | n = 12
 | f = \paren {p \lor q} \implies \paren {p \lor \paren {q \lor s} }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 3$
 | dep  = 10, 11
}}
{{TableauLine
 | n = 13
 | f = \paren {\paren {p \lor q} \implies \paren {p \lor \paren {q \lor s} } } \implies \paren {\paren {r \lor \paren {p \lor q} } \implies \paren {r \lor \paren {p \lor \paren {q \lor s} } } }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 4$
 | c = $r \,/\, p, \paren {p \lor q} \,/\, q, \paren {p \lor \paren {q \lor s} } \,/\, r$
}}
{{TableauLine
 | n = 14
 | f = \paren {r \lor \paren {p \lor q} } \implies \paren {r \lor \paren {p \lor \paren {q \lor s} } }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 3$
 | dep  = 12, 13
}} <!-- D7 -->
{{TableauLine
 | n = 15
 | f = \paren {\paren {p \lor q} \lor \paren {q \lor r} } \implies \paren {\paren {p \lor \paren {q \lor r} } \lor \paren {p \lor q} }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 1$
 | dep = 8
 | c = $\paren {p \lor q} \,/\, p, \paren {q \lor r} \,/\, q, p \,/\, r$
}}
{{TableauLine
 | n = 16
 | f = \paren {\paren {p \lor \paren {q \lor r} } \lor \paren {p \lor q} } \implies \paren {\paren {p \lor \paren {q \lor r} } \lor \paren {p \lor \paren {q \lor r} } }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 1$
 | dep = 14
 | c = $\paren {p \lor \paren {q \lor r} } \,/\, r, r \,/\, s$
}}
{{TableauLine
 | n = 17
 | f = \paren {\paren {p \lor \paren {q \lor r} } \lor \paren {p \lor \paren {q \lor r} } } \implies \paren {p \lor \paren {q \lor r} }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 1$
 | c = $\paren {p \lor \paren {q \lor r} } \,/\, p$
}}
{{TableauLine
 | n = 18
 | f = \paren {\paren {p \lor q} \lor \paren {q \lor r} } \implies \paren {\paren {p \lor \paren {q \lor r} } \lor \paren {p \lor \paren {q \lor r} } }
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep  = 15, 16
}}
{{TableauLine
 | n = 19
 | f = \paren {\paren {p \lor q} \lor \paren {q \lor r} } \implies \paren {p \lor \paren {q \lor r} }
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep  = 17, 18
}}<!-- D8 -->
{{TableauLine
 | n = 20
 | f = \paren {\paren {p \lor q} \lor r} \implies \paren {p \lor \paren {q \lor r} }
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep  = 3, 19
}}<!-- D9 -->
{{EndTableau}}
{{qed}}