Proof for ∨ distributing over → I'm am stuggling to prove the following:
x ∨ ( y → z ) ≡ ( x ∨ y ) → ( x ∨ z )
After making a truth table, I know that disjunction distributes over implication but I am failing to prove the above equation using theorems.
Thank you for any help.
 A: Here is a full answer using Git Gud's approach, which is just sound advice: if you need to prove an equality or equivalence, then start at the most complex side and treat it as a simplification problem.$
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}}
\newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} }
\newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{\ref}[1]{\text{(#1)}}
\newcommand{\then}{\rightarrow}
\newcommand{\when}{\leftarrow}
\newcommand{\true}{\text{true}}
\newcommand{\false}{\text{false}}
$
And specifically for propositional logic, it is helpful to know that it is often helpful to expand $\;P \then Q\;$, and that there are three basic ways to do that: $\;\lnot P \lor Q\;$, or $\;P \equiv P \land Q\;$, or $\;P \lor Q \equiv Q\;$.
So we start at the right hand side, and calculate as follows:
$$\calc
    (x \lor y) \then (x \lor z)
\op=\hint{expand $\;\then\;$ in the shortest way possible}
    \lnot (x \lor y) \lor x \lor z
\op=\hint{DeMorgan -- this looks like the simplest way to make progress}
    (\lnot x \land \lnot y) \lor x \lor z
\op=\hint{distribute $\;x\;$ over the left hand part -- brings the $\;x\;$'s together}
    ((\lnot x \lor x) \land (\lnot y \lor x)) \lor z
\op=\hint{excluded middle; simplify}
    \lnot y \lor x \lor z
\op=\hint{reorder disjuncts; re-introduce $\;\then\;$}
    x \lor (y \then z)
\endcalc$$
This completes the proof that $\;\lor\;$ distributes over $\;\then\;$.
A: We have the following, $$
\begin{align}
x \lor ( y \to z ) 
&
\equiv 
x\lor(\lnot y\lor z) 
\\
&
\equiv
(x\lor \lnot y)\lor z
\\
&
\equiv
\big({\mathtt{T}}\land(x\lor \lnot y)\big)\lor z
\\
&
\equiv
\big((\lnot x\lor x)\land(x\lor \lnot y)\big)\lor z
\\
&
\equiv
\big(x\lor (\lnot x\land \lnot y)\big)\lor z
\\
&
\equiv
\big((\lnot x\land \lnot y)\lor x\big)\lor z
\\
&
\equiv
(\lnot x\land \lnot y)\lor (x\lor z)
\\
&
\equiv
\lnot(x\lor y)\lor (x\lor z)
\\
&
\equiv
( x \lor y ) \to ( x \lor z ).\tag*{$\square$}
\end{align}$$
