An axiomatization question

Consider the following set of identities (quantified over all variables) on the language {→, 1}:

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

Is the following identity derivable from the above identities?

(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)))