The Logic E

Here is a Hilbert-style axiomatisation of the logic $$\mathbf{E}$$ of relevant entailment.

Our language contains propositional variables, parentheses, negation, conjunction, and implication. In addition, we use the following defined connectives:

\begin{align} A\vee B &=_{df} \neg(\neg A \amp \neg B) \\ A \leftrightarrow B &=_{df} (A \rightarrow B) \amp(B \rightarrow A) \end{align}
 Axiom Scheme Axiom Name 1. $$A \rightarrow A$$ Identity 2. $$((A \rightarrow A) \rightarrow B) \rightarrow B$$ EntT 3. $$(A \rightarrow B) \rightarrow((B \rightarrow C) \rightarrow(A \rightarrow C))$$ Suffixing 4. $$(A \rightarrow(A \rightarrow B)) \rightarrow(A \rightarrow B)$$ Contraction 5. $$(A \amp B) \rightarrow A,(A \amp B) \rightarrow B$$ & -Elimination 6. $$A \rightarrow(A\vee B), B \rightarrow(A\vee B)$$ $$\vee$$-Introduction 7. $$((A \rightarrow B) \amp(A \rightarrow C)) \rightarrow(A \rightarrow(B \amp C))$$ & -Introduction 8. $$((A\vee B) \rightarrow C)\leftrightarrow((A \rightarrow C) \amp(B \rightarrow C))$$ $$\vee$$-Elimination 9. $$(A \amp(B\vee C)) \rightarrow((A \amp B)\vee(A \amp C))$$ Distribution 10. $$(A \rightarrow \neg B) \rightarrow(B \rightarrow \neg A)$$ Contraposition 11. $$\neg \neg A \rightarrow A$$ Double Negation
 Rule Name 1. $$A \rightarrow B, A\vdash B$$ Modus Ponens 2. $$A, B\vdash A \amp B$$ Adjunction