let Y be non empty set ; :: thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nand' (b 'xor' c) = (a '&' b) 'eqv' (a '&' c)
let a, b, c be Function of 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 Th11
.= 'not' ('not' ((a '&' b) 'eqv' (a '&' c))) by BVFUNC_6:85
.= (a '&' b) 'eqv' (a '&' c) ; :: thesis: verum