theorem :: BVFUNC_1:68

for x, y, z being boolean object st z => (y => x) = TRUE holds
y => (z => x) = TRUE ;