Prove that $B ⇒ (C ⇒ D) ⊢ C ⇒ (B ⇒ D)$ I want to prove $B ⇒ (C ⇒ D) ⊢ C ⇒ (B ⇒ D)$ by the use of the following three axioms and modus ponens:
$$(A1):(B ⇒ (C ⇒B ))$$
$$(A2):((B ⇒ (C ⇒D )) ⇒ ((B ⇒C ) ⇒ (B ⇒D )))$$
$$(A3):(((¬C ) ⇒ (¬B )) ⇒(((¬C ) ⇒B) ⇒C ))$$
So far my thought process is that I need to get the desired expression on the right side of the statement form and then show that the left side is a tautology using the axioms, therefore by modus ponens the right side is true. Is this a correct way of thinking? How should I approach questions such as these?
 A: I use Polish notation.
The formation rules run:


*

*All lower case letters of the Latin alphabet qualify as wffs.

*If $\alpha$ and $\beta$ qualify as wffs, so do N$\alpha$, and C$\alpha$$\beta$.


The axioms in Polish notation run:


*

*CpCqp

*CCpCqrCCpqCpr

*CCNpNqCCNpqp


And the problem goes:
CbCcd $\vdash$ CcCbd.
Neither CbCcd nor CcCbd consists of a tautology.
To prove this you want to produce a derivation which starts with CbCcd and ends with CcCbd using only modus ponens and uniform substitution for variables in axioms or theorems.  
To solve this you can start with CbCcd.
Next distribute it (or in other words apply A2 to CbCcd).  This gives you CCbcCbd.
Then prefix what you just had with a variable where you can make substitutions (or in other words apply A1 to what you just got).  This gives you CpCCbcCbd, where you can substitute wffs for p, but not for b, c, or d.
Next distribute what you just had.  This gives you CCpCbcCpCbd.
Finally, apply the formula you just obtained to A1.  Since you can only substitute for p, this means that CpCbc has to become CcCbc.  So once you apply CCpCbcCpCbd to CpCqp, CpCqp becomes CcCbc and you detach CcCbd.
