Properties semantic equivalence proof - too many steps. I would like to prove
$$(p ⇒ q) ⇒ r ≡ (r \vee p) ∧ (q ⇒ r)$$
Have I used too many steps? It seems long. Mind you I do want to show each step individually so implication in two separate steps for example is required. I am asked to show simple steps like commutativity.
implication
$  (¬p \vee q) ⇒ r$
implication 
$  ¬(¬ p \vee q) \vee r$
DeMorgans
$ (¬¬p ∧ ¬q) \vee r$
double negation
$ (¬ p ∧ ¬q) \vee r$
commutativity
$ r \vee (¬ p ∧ ¬q)$
distributivity
$(r \vee p) ∧ (r \vee ¬q)$
commutativity
$  (r \vee p) ∧ (¬q \vee r )  $
implication
$  (r \vee p) ∧ (¬q  ⇒ r ) $
thank you in advance  
 A: Following André's observation, we could also give a semantic justification. 
Consider an arbitrary truth-assignment $\mathcal M$ s.t.: $$\mathcal{M} \models (p \rightarrow q) \rightarrow r)_{(1)}.$$ From (1) we know that: $$\mathcal M \not\models p \rightarrow q_{(1_L)} \text{ or } \mathcal M \models r_{(1_R)}.$$
($1_L$) means that $\mathcal M \models p$ and $\mathcal M \not\models q$, which when distributed with ($1_R$) tells us that: $$\mathcal M \models p \lor r_{(2_L)} \text{ and } \mathcal M \models \lnot q \lor r_{(2_R)}.$$
Commuting the disjuncts in $(2_L)$ and applying the definition of $\rightarrow$ in ($2_R$) we obtain:  $$\mathcal M \models r \lor p \text{ and } \mathcal M \models q \rightarrow r.$$
Combining the conjuncts we obtain the desired conclusion, i.e.: $\mathcal{M} \models (r \lor p)\land (q \rightarrow r)$. 
A: We start from $(p\rightarrow q) \rightarrow r$ and as you did, we can use the definition of implication to get
$$ \equiv (¬p \vee q) \rightarrow r$$
Using implication again, we get
$$ \equiv  ¬(¬ p \vee q) \vee r$$
As as you invoked, from DeMorgan's we know
$$ \equiv (¬¬p \land ¬q) \vee r$$
So far so good. Now, we can certainly invoke double negation, but correctly applied it gives us
$$\equiv (p\land ¬q) \vee r$$
We can commute to get
$$\equiv r \vee (p \land ¬q)$$
And by the distributive rule, we obtain
$$\equiv(r \vee p) \land (r \vee ¬q)$$
Sure, we can commute again (very often we can use commutativity and associativity without listing those as separate steps)
$$ \equiv (r \vee p) \land (¬q \vee r )  $$
Now, by the definition of implication, we know that $\lnot q \lor r \equiv q \rightarrow r$, so you we need to eliminate the negation of $q$ when transforming the second term into an implication:
$$ \equiv (r \vee p) \land (q  \rightarrow r ) $$
