If A→(B∧C), Prove (D→A) → (D→C) without using conditional proof The conditional proof version of this is pretty easy. However, solving this without conditional proof seems to be quite difficult.
I tried to turn the premise into:


*

*~A v (B∧C)

*(~AvB) ∧ (~AvC)
I tried to use disjunction introduction to transform (~AvC) into (D→A) → (D→C) but failed. 
Any ideas on how should I proceed? Maybe disjunction introduction is not the right way to deal with this problem?
 A: 1) $A \to (B \land C)$ --- premise
2) $\lnot A \lor (B \land C)$ --- from 1) by Material implication
3) $(\lnot A \lor B) \land (\lnot A \lor C)$ --- from 2) by Distributivity
4) $(\lnot A \lor C)$ --- from 3) by Conjunction elimination
5) $(\lnot A \lor C) \lor \lnot D$ --- from 4) by Disjunction introduction
6) $[(\lnot D \lor C) \lor D] \land [(\lnot D \lor C) \lor \lnot A]$ --- from 5) using : $[(\lnot A \lor C) \lor \lnot D] \equiv [(\lnot A \lor C) \lor \lnot D] \land TRUE$ and : $TRUE \equiv (D \lor \lnot D) \lor C$ and Associativity and Commutativity
7) $(\lnot D \lor C) \lor (D \land \lnot A)$ --- from 6) by Distributivity
8) $\lnot (\lnot D \lor A) \lor (\lnot D \lor C)$ --- from 7) by De Morgan
9) $(\lnot D \lor A) \to (\lnot D \lor C)$ --- from 9) by Material implication

10) $(D \to A) \to (D \to C)$ --- from 9) by Material implication.


Of course, with Natural Deduction the proof is much more easier.
A: You can prove this through what might get called "prefixing" CCpqCCrpCrq, which isn't too far away in terms of condensed detachment from the axiom set.
I use Polish notation.  The formation rules are:


*

*All letters of the Latin alphabet are well-formed formulas.

*If $\alpha$ and $\beta$ qualify as well-formed formulas, so does C$\alpha$$\beta$ and K$\alpha$$\beta$.


So, we want to prove CaKbc $\vdash$ CCdaCdc.
The axioms I'll use are CpCqp - Recursive Variable Prefixing, CCpCqrCCpqCpr - C-Self Distribution, CKpqq - right conjunction elimination.  I also use condensed detachment.  Note we can make substitutions for any letters, except for a, b, c, and d in the following.
axiom      1 CpCqp
axiom      2 CCpCqrCCpqCpr
axiom      3 CKpqq
D1.2       4 CpCCqCrsCCqrCqs
D2.4       5 CCpCqCrsCpCCqrCqs
D5.1       6 CCpqCCrpCrq
assumption 7 CaKbc
D6.3       8 CCpKqrCpr
D8.7       9 Cac
D6.9      10 CCpaCpc

And CCpaCpc comes as a more general well-formed formula of the special case CCdaCdc.
