theorem :: BVFUNC_1:69

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