Ways to prove $P\implies Q$ Suppose $P\implies Q$ is to be proven, where $P$ and $Q$ are two statements. Can it be proven as follows:
We take the following together:

*

*$P$

*negation of $Q$
Then, we proceed with these two things. We reach at a state where we conclude that “negation of $Q$“ fails to hold. Or, we reach at a state where we conclude that $P$ fails to hold.  Then, can we say the proof is done?
 A: Yes. In the first case, "negation of $Q$ failing to hold" is equivalent to "$Q$ holding", so in that case you have proven that, under $P$, $Q$ always holds. In the second case, you have done the same, you have proven that $\neg Q\implies\neg P$, which is the same as $P\implies Q$.
A: $$P\rightarrow Q\\\lnot P\lor Q\\\lnot P\lor \lnot(\lnot Q)$$
Since the three propositions above are tautologically equivalent to one another (easily verifiable using their truth tables), proving the statement $P\implies Q$ is indeed equivalent to proving that

*

*either $P$ fails to hold

*or the negation of $Q$ fails to hold.

A: In a Natural Deduction system for Classical Logic, the derivation of a contradiction under the assumptions of $P$ and $\lnot Q$ will suffice to deduce $P\to Q$.
$$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline #2\end{array}}\def\nfitch#1{\begin{array}{|l}#1\end{array}}\nfitch{~~\vdots\\~\fitch{~~h.~P}{\fitch{~~i.~\lnot Q}{~~~\vdots\\~~j.~\bot\hspace{11ex}\text{somehow}}\\~~k.~\lnot\lnot Q\hspace{10ex}\lnot\mathsf I~i{-}j\\~~\ell.~Q\hspace{13ex}\lnot\lnot\mathsf E~k}\\~~m.~P\to Q\hspace{9ex}{\to}\mathsf I~{h{-}\ell}}$$
Note: Any valid contradiction will do, whether it is a contradiction of either assumption, or something else.
