let Y be non empty set ; :: thesis: for a, b, c being Element of Funcs (Y,BOOLEAN) holds a 'nand' (b 'xor' c) = (a '&' b) 'eqv' (a '&' c)
let a, b, c be Element of Funcs (Y,BOOLEAN); :: thesis: a 'nand' (b 'xor' c) = (a '&' b) 'eqv' (a '&' c)
thus a 'nand' (b 'xor' c) = 'not' (a '&' (b 'xor' c)) by Th1
.= 'not' ((a '&' b) 'xor' (a '&' c)) by BVFUNC25:11
.= 'not' ('not' ((a '&' b) 'eqv' (a '&' c))) by BVFUNC_8:12
.= (a '&' b) 'eqv' (a '&' c) ; :: thesis: verum