(z^x->y) -> z^(z^x->y) -> not(y) -> дизъюнкция -> + z^(z^x->y).
Вроде бы так, потому что, насколько помню, отрицание имеет высший приоритет, затем дизъюнкция и т.д.