theorem :: BVFUNC_1:70

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