:: Propositional Calculus for Boolean Valued Functions, I
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received March 13, 1999
:: 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 '&' ('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 ('not' b) 'imp' ('not' a) = 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' ('not' b) = 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 (('not' a) '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 (('not' a) 'imp' ('not' b)) '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' (('not' b) 'imp' ('not' a)) = 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' ('not' b)) 'imp' (b 'imp' ('not' a)) = I_el Y

proof end;

theorem :: BVFUNC_5:34

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (('not' a) 'imp' b) 'imp' (('not' b) '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' ('not' a)) 'imp' ('not' a) = I_el Y

proof end;

theorem :: BVFUNC_5:36

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' a) '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) = (('not' a) 'or' ('not' b)) 'or' ('not' c)

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) = (('not' a) '&' ('not' b)) '&' ('not' 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;