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