An axiomatization question

Consider the following class of n-potent BCK-algebras. The language is {→, 1} and is of type ⟨2, 0⟩; the axioms are as follows (quantified over all variables):

(x → y) → ((y → z) → (x → z)) = 1 x → 1 = 1 1 → x = x x → y = 1 and y → x = 1 ⇒ x = y x → (x → (x → y))) = x → (x → y)

(The quasi-identity above may be replaced by the identity:

(y → x)^{2} → ((x → y)^{2} → x) = (y → x)^{2} → ((x → y)^{2} → y),

where z^{2} → w = z → (z → w).)

Problem: Is the following identity derivable from the above:

(x → (x → z)) → ((y → (y → z)) → (x → (y → z))) = 1

Alternatively, consider the Hilbert style deductive system with → as its only connective axiomatized by:

⊢ (x → y) → ((y → z) → (x → z)) ⊢ (x → (y → z)) → (y → (x → z)) ⊢ x → (y → x) ⊢ [x → (x → (x → y)))] → [x → (x → y)] x, x → y ⊢ y

Is the following formula derivable in the above logic?

(x → (x → z)) → ((y → (y → z)) → (x → (y → z)))