On page 7 in the article referred to below an axiom $D9$ is stated as follows: $$A\to B\to.\lnot(A \& \lnot B)~\\ (\text{equivalently: } (A\to\lnot A)\to\lnot A)$$


How may one prove the alleged equivalence, using the rest of the axioms and the inference rules:


D1: $\vdash A\to A$


D2: $\vdash((A\to B)\wedge(B\to C))\to(A\to C)$


D3: $\vdash(A\wedge B)\to A$


D4: $\vdash(A\wedge B)\to B$


D5: $\vdash((A\to B)\wedge (A\to C))\to(A\to (B\wedge C))$


D6: $\vdash(A\wedge(B\vee C))\to ((A\wedge B)\vee(A\vee C))$


D7: $\vdash\lnot\lnot A\to A$


D8: $ \vdash(A\to\lnot B)\to(B\to\lnot A)$


R1: $\vdash A \ \& \vdash (A\to B) \Rightarrow \ \vdash B$


R2: $\vdash A \ \& \vdash B \Rightarrow \ \vdash A\wedge B$


R3: $\vdash A\to B \ \& \ \vdash C\to D\ \Rightarrow \ \vdash(B\to C)\to (A\to D)$


Dialectical Logic, Classical Logic, and the Consistency of the World
Author(s): Richard Routley and Robert K. Meyer
Source: Studies in Soviet Thought , Jun., 1976, Vol. 16, No. 1/2 (Jun., 1976), pp. 1-25. [Link (behind JSTOR paywall)](https://www.jstor.org/stable/20098681?seq=1)



Counterexample equivalent in relevant logic DL
From D3 and D4,


1- $A\wedge\neg B\rightarrow A$.


2- $A\wedge\neg B\rightarrow \neg B$.


From 2, D8 and R1,


3- $B\rightarrow \neg(A\wedge\neg B)$.


From 1, 3 and R3 (taking $B=A$, $C=B$, $A=A\wedge\neg B$ and $D=\neg(A\wedge\neg B)$)


4- $(A\rightarrow B)\rightarrow (A\wedge\neg B\rightarrow \neg(A\wedge\neg B))$.


From the axiom $(A\rightarrow \neg A)\rightarrow A)$,


5- $(A\wedge\neg B\rightarrow\neg(A\wedge\neg B))\rightarrow\neg(A\wedge\neg B)$.


From 4, 5, by transitivity of implication (D2, R1, R2),


6- $(A\rightarrow B)\rightarrow \neg(A\wedge\neg B)$.


The converse implication is simpler. Take $B=\neg A$ in $(A\rightarrow B)\rightarrow \neg(A\wedge\neg B)$. Then,


1- $(A\rightarrow \neg A)\rightarrow \neg(A\wedge\neg\neg A)$.


From D5, using the double negation law (easily obtained from D8 and R1)


2- $A\rightarrow (A\wedge\neg\neg A)$, so $A\rightarrow\neg\neg(A\wedge\neg\neg A)$ (the double negation law once more.)


From D8,


3- $(A \rightarrow\neg\neg(A\wedge\neg\neg A))\rightarrow (\neg(A\wedge\neg\neg A)\rightarrow\neg A))$.


From 2, 3 and R1,


4- $\neg(A\wedge\neg\neg A)\rightarrow \neg A$.


The conclusion follows from 1, 4 and the transitivity of implication.


