Logic – Provability of $(\phi\implies\psi) \iff ((\phi\land\psi)\lor \neg\phi)$ in Hilbert Calculus

Question

Is $(\phi\implies \psi) \iff ((\phi\land \psi)\lor \neg \phi) $ in the following hilbert calculus without contraposition or reductio ad absurdum? If so, how would I go about proving it, and if not, how would I prove that it is not derivable?

Inference Rules: Modus Ponens

Axioms:

$\phi \implies (\psi \implies \phi)$

$(\phi \implies (\chi \implies \psi)) \implies ((\phi \implies \chi) \implies (\phi \implies \psi))$

$(\phi \land \psi)\implies\phi; (\phi \land \psi) \implies \psi $

$\phi \implies (\psi \implies (\phi \land \psi)) $

$\phi \implies (\phi \lor \psi); \psi \implies (\phi \lor \psi) $

$(\phi \implies \psi) \implies ((\chi \implies \psi) \implies ((\phi \lor \chi) \implies \psi)) $

Biimplication is defined as usual.

$\phi\iff\neg\neg\phi $

$\neg (\phi \land \psi) \iff (\neg \phi \lor \neg \psi) $

$\neg (\phi \lor \psi) \iff (\neg \phi \land \neg \psi) $

$\phi \lor \neg \phi $

Here is my current attempt at proving one side of the conditional

Answer 1

The following tables satisfy the above axioms:

Tables

{1, 2} are the designated values.

Counterexample at 2, 3. ((ϕ ∧ ψ) ∨ ¬ϕ) is designated there but (ϕ⟹ψ) is not. Therefore the other side of the biconditional is not provable in this logic. □