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