I am trying to prove the fact $A \supset B, A \supset C \vdash A \supset (B \land C)$ in a hilbert-type system. However, I am struggling to find a translation rule for $B \land C$.
Citing from my textbook:
We introduce other connectives [besides $\supset$] by definition: $$(D1) \quad(B \land C) \text{ for } \lnot(B\supset \lnot C)$$ [...] The meaning of $(D1)$, for example, is that for any [well-formed formulas] $B$ and $C$, "$(B \land C)$" is an abbreviation for "$\lnot(B\supset C)$".
The definition of course makes sense, but how do I cast this into a useable rule for the calculus?
Semantically, it would be correct to conclude that $A \supset \lnot(B \supset \lnot C) \vdash A \supset (B \land C) $ but can I just replace one with the other in the calculus?
Or should I start with a simple rule like $\lnot(B\supset \lnot C) \vdash (B \land C)$ and somehow include that in my proof?