let Y be non empty set ; :: thesis: for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d)
let a, b, c, d be Function of Y,BOOLEAN; :: thesis: ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d)
A1: ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) '&' (c 'imp' d) by Th12
.= ((a 'imp' b) '&' (b 'imp' c)) '&' ((a 'imp' c) '&' (c 'imp' d)) by BVFUNC_1:4
.= ((a 'imp' b) '&' (b 'imp' c)) '&' (((a 'imp' c) '&' (c 'imp' d)) '&' (a 'imp' d)) by Th12
.= (((a 'imp' b) '&' (b 'imp' c)) '&' ((a 'imp' c) '&' (c 'imp' d))) '&' (a 'imp' d) by BVFUNC_1:4
.= ((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_1:4
.= (((a 'imp' b) '&' ((b 'imp' c) '&' (c 'imp' d))) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_1:4
.= (((a 'imp' b) '&' (((b 'imp' c) '&' (c 'imp' d)) '&' (b 'imp' d))) '&' (a 'imp' c)) '&' (a 'imp' d) by Th12
.= ((((a 'imp' b) '&' ((b 'imp' c) '&' (c 'imp' d))) '&' (b 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_1:4
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (b 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_1:4
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (b 'imp' d)) '&' (a 'imp' d) by BVFUNC_1:4
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d)) '&' (b 'imp' d) by BVFUNC_1:4 ;
((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d) = ((('not' a) 'or' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d) by BVFUNC_4:8
.= ((('not' a) 'or' ((b '&' c) '&' d)) '&' (('not' b) 'or' (c '&' d))) '&' (c 'imp' d) by BVFUNC_4:8
.= ((('not' a) 'or' ((b '&' c) '&' d)) '&' (('not' b) 'or' (c '&' d))) '&' (('not' c) 'or' d) by BVFUNC_4:8
.= ((((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' (c '&' d))) '&' (('not' c) 'or' d) by BVFUNC_5:39
.= ((((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' ((('not' b) 'or' c) '&' (('not' b) 'or' d))) '&' (('not' c) 'or' d) by BVFUNC_1:11
.= (((((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' c)) '&' (('not' b) 'or' d)) '&' (('not' c) 'or' d) by BVFUNC_1:4
.= (((((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' b) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d)) '&' (('not' c) 'or' d) by BVFUNC_1:4
.= (((((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d)) '&' (('not' c) 'or' d) by BVFUNC_1:4
.= (((((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' c) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_1:4
.= (((((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' a) 'or' c)) '&' (('not' c) 'or' d)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_1:4
.= (((((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' d)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_1:4
.= (((((a 'imp' b) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' d)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (('not' c) 'or' d)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d)) '&' (b 'imp' d) by BVFUNC_4:8 ;
hence ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d) by A1; :: thesis: verum