Inference rules proof I'm supposed to write a formal proof given $(a \vee b) \rightarrow (c \rightarrow d), e,$ and $(b \wedge e) \rightarrow \neg d$, and I have to show that $b \rightarrow \neg c$. I have no idea where to start with this, as I'm very new to inference and equivalence proofs, so any help/explanation how to begin on this would be really great.
 A: $$(b\wedge e)\rightarrow \neg d\equiv \neg(b\wedge e)\vee \neg d\equiv\neg b\vee\neg e\vee\neg d\equiv\neg e\vee\neg b\vee\neg d.$$ But $e$ and so $\neg b\vee\neg d$ by disjunctive syllogism. Also 
$$(a\vee b)\rightarrow (c\rightarrow d)\equiv (a\rightarrow(c\rightarrow d))\wedge(b\rightarrow(c\rightarrow d))$$ so $b\rightarrow(c\rightarrow d)$ by simplification. But $$b\rightarrow(c\rightarrow d)\equiv \neg b\vee(\neg c\vee d)\equiv (\neg b\vee\neg c)\vee d$$ and so by resolution $$\neg b\vee(\neg b\vee\neg c)\equiv\neg b\vee\neg c\equiv b\rightarrow\neg c$$
A: Hint: Use a direct proof (approx. 12 lines). Begin by supposing $b$ is true. Then you can immediately infer that $a\lor b$ is true. Eventually, you should be able conclude that $\neg c$ is true. 
A: Here are two proofs, one uses a Fitch-style natural deduction proof checker and the other is a generated tree proof. 
The proof checker requires one to enter each line manually, but it offers a way to verify that each line is correct. This may be the best tool to use to learn the inference rules provided a proof can be constructed. 
The tree proof provides a proof or a countermodel if a proof cannot be constructed. This may be best if one cannot find a proof and wants to know if a countermodel might exist. One can also use a truth table generator for a similar purpose.
Here is the natural deduction proof:

Here is a tree proof:

Links to the proof checker, the forallx textbook and the tree proof generator are below.

Tree Proof Generator Generated on July 27, 2019 at https://www.umsu.de/logik/trees/
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf
