theorem :: BVFUNC_1:49

for x, y, z being boolean object holds x 'nand' (y '&' z) = (x '&' y) 'nand' z ;