:: Propositional Calculus for Boolean Valued Functions, I
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Copyright (c) 1999-2021 Association of Mizar Users

theorem :: BVFUNC_5:1
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( ( a = I_el Y & b = I_el Y ) iff a '&' b = I_el Y )
proof end;

theorem Th2: :: BVFUNC_5:2
for Y being non empty set
for b being Function of Y,BOOLEAN st (I_el Y) 'imp' b = I_el Y holds
b = I_el Y
proof end;

theorem :: BVFUNC_5:3
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a = I_el Y holds
a 'or' b = I_el Y
proof end;

theorem :: BVFUNC_5:4
for Y being non empty set
for a, b being Function of Y,BOOLEAN st b = I_el Y holds
a 'imp' b = I_el Y
proof end;

theorem :: BVFUNC_5:5
for Y being non empty set
for a, b being Function of Y,BOOLEAN st 'not' a = I_el Y holds
a 'imp' b = I_el Y
proof end;

theorem :: BVFUNC_5:6
for Y being non empty set
for a being Function of Y,BOOLEAN holds 'not' (a '&' ()) = I_el Y
proof end;

theorem :: BVFUNC_5:7
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' a = I_el Y
proof end;

theorem :: BVFUNC_5:8
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a 'imp' b = I_el Y iff () 'imp' () = I_el Y )
proof end;

theorem :: BVFUNC_5:9
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' b = I_el Y & b 'imp' c = I_el Y holds
a 'imp' c = I_el Y
proof end;

theorem :: BVFUNC_5:10
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a 'imp' b = I_el Y & a 'imp' () = I_el Y holds
'not' a = I_el Y
proof end;

theorem :: BVFUNC_5:11
for Y being non empty set
for a being Function of Y,BOOLEAN holds (() 'imp' a) 'imp' a = I_el Y
proof end;

theorem :: BVFUNC_5:12
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (('not' (b '&' c)) 'imp' ('not' (a '&' c))) = I_el Y
proof end;

theorem :: BVFUNC_5:13
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((b 'imp' c) 'imp' (a 'imp' c)) = I_el Y
proof end;

theorem Th14: :: BVFUNC_5:14
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' b = I_el Y holds
(b 'imp' c) 'imp' (a 'imp' c) = I_el Y
proof end;

theorem Th15: :: BVFUNC_5:15
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds b 'imp' (a 'imp' b) = I_el Y
proof end;

theorem :: BVFUNC_5:16
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) 'imp' c) 'imp' (b 'imp' c) = I_el Y
proof end;

theorem :: BVFUNC_5:17
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds b 'imp' ((b 'imp' a) 'imp' a) = I_el Y
proof end;

theorem :: BVFUNC_5:18
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (c 'imp' (b 'imp' a)) 'imp' (b 'imp' (c 'imp' a)) = I_el Y
proof end;

theorem :: BVFUNC_5:19
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (b 'imp' c) 'imp' ((a 'imp' b) 'imp' (a 'imp' c)) = I_el Y
proof end;

theorem :: BVFUNC_5:20
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (b 'imp' (b 'imp' c)) 'imp' (b 'imp' c) = I_el Y
proof end;

theorem Th21: :: BVFUNC_5:21
for Y being 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
proof end;

theorem :: BVFUNC_5:22
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a = I_el Y holds
(a 'imp' b) 'imp' b = I_el Y
proof end;

theorem :: BVFUNC_5:23
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st c 'imp' (b 'imp' a) = I_el Y holds
b 'imp' (c 'imp' a) = I_el Y
proof end;

theorem :: BVFUNC_5:24
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st c 'imp' (b 'imp' a) = I_el Y & b = I_el Y holds
c 'imp' a = I_el Y
proof end;

theorem Th25: :: BVFUNC_5:25
for Y being non empty set
for a being Function of Y,BOOLEAN st (I_el Y) 'imp' ((I_el Y) 'imp' a) = I_el Y holds
a = I_el Y
proof end;

theorem :: BVFUNC_5:26
for Y being non empty set
for b, c being Function of Y,BOOLEAN st b 'imp' (b 'imp' c) = I_el Y holds
b 'imp' c = I_el Y
proof end;

theorem :: BVFUNC_5:27
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' (b 'imp' c) = I_el Y holds
(a 'imp' b) 'imp' (a 'imp' c) = I_el Y
proof end;

theorem :: BVFUNC_5:28
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' (b 'imp' c) = I_el Y & a 'imp' b = I_el Y holds
a 'imp' c = I_el Y
proof end;

theorem :: BVFUNC_5:29
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' (b 'imp' c) = I_el Y & a 'imp' b = I_el Y & a = I_el Y holds
c = I_el Y
proof end;

theorem :: BVFUNC_5:30
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'imp' (b 'imp' c) = I_el Y & a 'imp' (c 'imp' d) = I_el Y holds
a 'imp' (b 'imp' d) = I_el Y
proof end;

theorem :: BVFUNC_5:31
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (() 'imp' ()) 'imp' (b 'imp' a) = I_el Y
proof end;

theorem :: BVFUNC_5:32
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (() 'imp' ()) = I_el Y
proof end;

theorem :: BVFUNC_5:33
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' ()) 'imp' (b 'imp' ()) = I_el Y
proof end;

theorem :: BVFUNC_5:34
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (() 'imp' b) 'imp' (() 'imp' a) = I_el Y
proof end;

theorem :: BVFUNC_5:35
for Y being non empty set
for a being Function of Y,BOOLEAN holds (a 'imp' ()) 'imp' () = I_el Y
proof end;

theorem :: BVFUNC_5:36
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds () 'imp' (a 'imp' b) = I_el Y
proof end;

theorem :: BVFUNC_5:37
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds 'not' ((a '&' b) '&' c) = (() 'or' ()) 'or' ()
proof end;

theorem :: BVFUNC_5:38
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds 'not' ((a 'or' b) 'or' c) = (() '&' ()) '&' ()
proof end;

theorem :: BVFUNC_5:39
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds a 'or' ((b '&' c) '&' d) = ((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d)
proof end;

theorem :: BVFUNC_5:40
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds a '&' ((b 'or' c) 'or' d) = ((a '&' b) 'or' (a '&' c)) 'or' (a '&' d)
proof end;