How to prove this tautology using equivalences? I am trying to prove that the following is a tautology:
$(A \implies (B \implies C)) \implies ((A \implies (C \implies D)) \implies (A \implies (B \implies D)))$
To make progress, I thought I'd eliminate all the arrows. After that, and some de Morgan, I've arrived at:
$(A \land B \land ¬C) \lor (A \land ¬C \land ¬D) \lor (¬A \lor B \lor D) $
At this point, I don't know how to carry on, though. I feel like I'm missing some rule -- I get stuck in trying to expand this and don't get anywhere.
I'd be really grateful for help / hints!
EDIT:
Thank you Henning Makholm and Mauro ALLEGRANZA for spotting mistakes in my reformulations. The rewritten form should read:
$(A \land B \land ¬C) \lor (A \land C \land ¬D) \lor (¬A \lor ¬B \lor D) $

(If anyone wants a proof by the deduction theorem)
Suppose $(A\implies (B\implies C))$. Then not $A$ or $(B \implies C)$.
Case 1: If not $A$,  then $(A⟹(B⟹D))$. So $((A⟹(C⟹D))⟹(A⟹(B⟹D)))$ is true.
Case 2: $A$ is true. So $(B \implies C)$, then not $B$ or $C$.
Case a) If not $B$,  then  $(A⟹(B⟹D))$ is true.
Case b) $B$. So $C$.
Case bi) If $D$ is false, $C⟹D$ is false, so $(A⟹(C⟹D))$ is false. So $((A⟹(C⟹D))⟹(A⟹(B⟹D)))$ is true.
bii) If $D$ is true, $B⟹D$ is true. So  $(A⟹(B⟹D))$  is true. So $((A⟹(C⟹D))⟹(A⟹(B⟹D)))$ is true.
So  $(A⟹(B⟹C)) \implies ((A⟹(C⟹D))⟹(A⟹(B⟹D)))$. 
