theorem :: BVFUNC_6:101

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (((a 'imp' c) '&' (b 'imp' d)) '&' (('not' c) 'or' ('not' d))) 'imp' (('not' a) 'or' ('not' b)) = I_el Y