let Y be non empty set ; for a, b, c, d being Function of Y,BOOLEAN holds ((a '&' b) '&' c) 'imp' d = ((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)
let a, b, c, d be Function of Y,BOOLEAN; ((a '&' b) '&' c) 'imp' d = ((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)
let x be Element of Y; FUNCT_2:def 8 K11((((a '&' b) '&' c) 'imp' d),x) = K11((((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)),x)
(((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)) . x =
(((a 'imp' d) 'or' (b 'imp' d)) . x) 'or' ((c 'imp' d) . x)
by BVFUNC_1:def 4
.=
(((a 'imp' d) . x) 'or' ((b 'imp' d) . x)) 'or' ((c 'imp' d) . x)
by BVFUNC_1:def 4
.=
((('not' (a . x)) 'or' (d . x)) 'or' ((b 'imp' d) . x)) 'or' ((c 'imp' d) . x)
by BVFUNC_1:def 8
.=
((('not' (a . x)) 'or' (d . x)) 'or' (('not' (b . x)) 'or' (d . x))) 'or' ((c 'imp' d) . x)
by BVFUNC_1:def 8
.=
((('not' (a . x)) 'or' (d . x)) 'or' (('not' (b . x)) 'or' (d . x))) 'or' (('not' (c . x)) 'or' (d . x))
by BVFUNC_1:def 8
.=
((('not' (a . x)) 'or' ((d . x) 'or' ('not' (b . x)))) 'or' (d . x)) 'or' (('not' (c . x)) 'or' (d . x))
.=
(((('not' (a . x)) 'or' ('not' (b . x))) 'or' (d . x)) 'or' (d . x)) 'or' (('not' (c . x)) 'or' (d . x))
.=
((('not' (a . x)) 'or' ('not' (b . x))) 'or' ((d . x) 'or' (d . x))) 'or' (('not' (c . x)) 'or' (d . x))
by BINARITH:11
.=
(('not' ((a . x) '&' (b . x))) 'or' ((d . x) 'or' ('not' (c . x)))) 'or' (d . x)
.=
((('not' ((a . x) '&' (b . x))) 'or' ('not' (c . x))) 'or' (d . x)) 'or' (d . x)
.=
(('not' ((a . x) '&' (b . x))) 'or' ('not' (c . x))) 'or' ((d . x) 'or' (d . x))
by BINARITH:11
.=
('not' (((a '&' b) . x) '&' (c . x))) 'or' (d . x)
by MARGREL1:def 20
.=
('not' (((a '&' b) '&' c) . x)) 'or' (d . x)
by MARGREL1:def 20
.=
(((a '&' b) '&' c) 'imp' d) . x
by BVFUNC_1:def 8
;
hence
K11((((a '&' b) '&' c) 'imp' d),x) = K11((((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)),x)
; verum