theorem :: BVFUNC_1:48

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