theorem :: BVFUNC_6:154

for Y being non empty set
for a1, a2, a3, b1, b2, b3 being Function of Y,BOOLEAN holds ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) = ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3)