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