let Y be non empty set ; :: thesis: 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)
let a1, a2, a3, b1, b2, b3 be Function of Y,BOOLEAN; :: thesis: ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) = ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3)
((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3) = ('not' ((('not' b1) '&' ('not' b2)) '&' a3)) 'or' ((('not' a1) 'or' ('not' a2)) 'or' b3) by BVFUNC_4:8
.= ((('not' ('not' b1)) 'or' ('not' ('not' b2))) 'or' ('not' a3)) 'or' ((('not' a1) 'or' ('not' a2)) 'or' b3) by BVFUNC_5:37
.= (((b1 'or' b2) 'or' ('not' a3)) 'or' (('not' a1) 'or' ('not' a2))) 'or' b3 by BVFUNC_1:8
.= ((b1 'or' b2) 'or' ((('not' a1) 'or' ('not' a2)) 'or' ('not' a3))) 'or' b3 by BVFUNC_1:8
.= ((('not' a1) 'or' ('not' a2)) 'or' ('not' a3)) 'or' ((b1 'or' b2) 'or' b3) by BVFUNC_1:8
.= ('not' ((a1 '&' a2) '&' a3)) 'or' ((b1 'or' b2) 'or' b3) by BVFUNC_5:37
.= ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) by BVFUNC_4:8 ;
hence ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) = ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3) ; :: thesis: verum