let Y be non empty set ; :: thesis: for a, b, c being Element of Funcs (Y,BOOLEAN) holds ((a 'imp' b) 'imp' c) 'imp' (b 'imp' c) = I_el Y
let a, b, c be Element of Funcs (Y,BOOLEAN); :: thesis: ((a 'imp' b) 'imp' c) 'imp' (b 'imp' c) = I_el Y
b 'imp' (a 'imp' b) = I_el Y by Th16;
hence ((a 'imp' b) 'imp' c) 'imp' (b 'imp' c) = I_el Y by Th15; :: thesis: verum