[proofplan] We combine the two given derivations with a temporary assumption of $A$. From $A$ and the derivation of $A \to B$, implication elimination gives $B$; from $B$ and the derivation of $\neg B$, understood as $B \to \bot$, implication elimination gives $\bot$. Discharging the temporary assumption $A$ by implication introduction yields $A \to \bot$, which is exactly $\neg A$. [/proofplan] [step:Fix derivations of the two hypotheses from $\Gamma$] Let $\pi_1$ be a derivation of $A \to B$ whose undischarged assumptions all belong to $\Gamma$, and let $\pi_2$ be a derivation of $\neg B$ whose undischarged assumptions all belong to $\Gamma$. Since $\neg B$ abbreviates $B \to \bot$, the derivation $\pi_2$ is a derivation of $B \to \bot$ from $\Gamma$. [/step] [step:Assume $A$ temporarily and derive $B$] Introduce a temporary assumption $A$. Under the undischarged assumptions $\Gamma \cup \{A\}$, the derivation $\pi_1$ still gives $A \to B$. Applying implication elimination to $A \to B$ and the temporary assumption $A$, we obtain $B$. [guided] We now work inside a subderivation whose only new assumption is $A$. The derivation $\pi_1$ has only assumptions from $\Gamma$, so it may be reused inside this subderivation without introducing any assumption outside $\Gamma \cup \{A\}$. Thus, inside the subderivation, we have both $A \to B$ and $A$. The implication-elimination rule says that from a derivation of $A \to B$ and a derivation of $A$, one may infer $B$. Applying that rule here gives a derivation of $B$ from undischarged assumptions contained in $\Gamma \cup \{A\}$. [/guided] [/step] [step:Use $\neg B$ to derive falsity] Under the same undischarged assumptions $\Gamma \cup \{A\}$, the derivation $\pi_2$ gives $B \to \bot$. Applying implication elimination to $B \to \bot$ and the derived formula $B$, we obtain $\bot$. [guided] The formula $\neg B$ is not being used as a primitive connective here; by the convention in the statement, $\neg B$ means $B \to \bot$. Since $\pi_2$ derives $\neg B$ from $\Gamma$, it gives a derivation of $B \to \bot$ with no undischarged assumptions except formulas in $\Gamma$. In the previous step, still under the temporary assumption $A$, we derived $B$. Therefore implication elimination applies again: from $B \to \bot$ and $B$, we infer $\bot$. The undischarged assumptions of this derivation are still contained in $\Gamma \cup \{A\}$. [/guided] [/step] [step:Discharge the temporary assumption to obtain $\neg A$] We have derived $\bot$ from undischarged assumptions contained in $\Gamma \cup \{A\}$, where the only assumption not belonging to $\Gamma$ is the temporary assumption $A$. By implication introduction, discharging that occurrence of $A$, we obtain $A \to \bot$ from $\Gamma$. Since $\neg A$ abbreviates $A \to \bot$, this is a derivation of $\Gamma \vdash \neg A$. [/step]