theorem :: BVFUNC_4:13

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a 'imp' c) 'eqv' (b 'imp' d) = I_el Y