natural deduction proof Need help with the steps for natural deduction:

P1. $(A \rightarrow B) \rightarrow (C \rightarrow A)$
P2. $A \wedge (C \leftrightarrow B)$
P3. $(A \lor C) \to (A \to B)$
$\therefore B \vee A$

Similar to this answer below.

*

*$\neg(B \lor ~I) \to (\neg L \text{ & } J)$

*$\neg L \to (M \text{ & } B)$

*$\neg (B \lor \neg I) $ $\therefore  M \lor E$

*$\neg L \text{ & } J$ $1,3$, $MP$

*$\neg L$ $4,$ Simp

*$M \text{ & } B$ $2,5, MP$

*$M$ $6$, Simp

*$M \lor E$ $7$, Add

 A: With Natural Deduction :
i) $A \land (C \leftrightarrow B)$ --- premise 2. 
ii) $A$ --- from i) by $\land$-elimination (or Simplification)
iii) $A \lor B$ --- from ii) by $\lor$-introduction (or Addition)
Thus, from i) and iii) :


$A \land (C \leftrightarrow B) \vdash A \lor B$


(I've used the "turnstile" : $\vdash$ to denote the relation of derivability; thus $\Gamma \vdash \psi$ means that there is a derivation of the formula $\psi$ from the set of formulae $\Gamma$.)
The above derivation needs only premise 2; thus the same derivation holds with the three premises 1-3 :


$(A \rightarrow B) \rightarrow (C \rightarrow A), A \land (C \leftrightarrow B),  (A \lor C) \rightarrow (A \rightarrow B) \vdash A \lor B$


A: Goal: to prove $B\lor A$ from premises $(1-3)$.


*

*$(A \rightarrow B) \rightarrow (C \rightarrow A)$

*$A \land (C \leftrightarrow B)$

*$(A \lor C) \rightarrow (A \rightarrow B)$ 

We actually need only premise $(2)$.


*$A \land (C\leftrightarrow B)\quad $ (given premise)

*$A\quad\quad$ (from (2): $\land$-elimination, aka simplification)

*$A \lor B \quad$ (from (3): $\lor$-Introduction, aka addition)

*$B\lor A\quad$ (By commutativity of $\lor$) 
Hence, from the given premises (in particular, given premise $(2)$), we have derived $B\lor A$, as desired.
A: Note that you just need one from your three premises, namely, the premise two:

$A \wedge (C \leftrightarrow B)$

From this we can use the $\wedge E$ and "detach" $A$ from it:

$\frac{A \wedge (C \leftrightarrow B)}{A}(\wedge E)$

Then we simple we the disjunction introduction rule in order to get $A \vee B$:

$\frac{\frac{A \wedge (C \leftrightarrow B)}{A}(\wedge E)}{A \vee B}(\vee I)$

This shows that $(A \rightarrow B) \rightarrow (C \rightarrow A),A \wedge (C \leftrightarrow B), A \wedge (C \leftrightarrow B) \vdash A \vee B$ as required.
In the derivation above we procceded by natural deduction. In this deduction system as you can see that the premises $(A \rightarrow B) \rightarrow (C \rightarrow A)$ and $A \wedge (C \leftrightarrow B)$ here are superfluous, but the fact our proof did not require their use does not imply they cannot be used as hypothesis: superfluous information can always be added.
