:: BVFUNC25 semantic presentation

theorem :: BVFUNC25:1

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds 'not' (a 'imp' b) = a '&' ('not' b)

proof end;

theorem Th2: :: BVFUNC25:2

for Y being non empty set
for b, a being Element of Funcs Y,BOOLEAN holds (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y

proof end;

theorem Th3: :: BVFUNC25:3

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a 'imp' b = ('not' b) 'imp' ('not' a)

proof end;

theorem :: BVFUNC25:4

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a 'eqv' b = ('not' a) 'eqv' ('not' b)

proof end;

theorem Th5: :: BVFUNC25:5

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a 'imp' b = a 'imp' (a '&' b)

proof end;

theorem :: BVFUNC25:6

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a 'eqv' b = (a 'or' b) 'imp' (a '&' b)

proof end;

theorem :: BVFUNC25:7

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds a 'eqv' ('not' a) = O_el Y

proof end;

theorem :: BVFUNC25:8

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds a 'imp' (b 'imp' c) = b 'imp' (a 'imp' c)

proof end;

theorem :: BVFUNC25:9

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds a 'imp' (b 'imp' c) = (a 'imp' b) 'imp' (a 'imp' c)

proof end;

theorem :: BVFUNC25:10

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a 'eqv' b = a 'xor' ('not' b)

proof end;

theorem :: BVFUNC25:11

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds a '&' (b 'xor' c) = (a '&' b) 'xor' (a '&' c)

proof end;

theorem :: BVFUNC25:12

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a 'eqv' b = 'not' (a 'xor' b)

proof end;

theorem :: BVFUNC25:13

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds a 'xor' a = O_el Y

proof end;

theorem :: BVFUNC25:14

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds a 'xor' ('not' a) = I_el Y

proof end;

theorem :: BVFUNC25:15

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds (a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a

proof end;

theorem Th16: :: BVFUNC25:16

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b))

proof end;

theorem Th17: :: BVFUNC25:17

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds (a '&' b) 'or' (('not' a) '&' ('not' b)) = (('not' a) 'or' b) '&' (a 'or' ('not' b))

proof end;

theorem :: BVFUNC25:18

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c

proof end;

theorem :: BVFUNC25:19

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds a 'eqv' (b 'eqv' c) = (a 'eqv' b) 'eqv' c

proof end;

theorem :: BVFUNC25:20

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds ('not' ('not' a)) 'imp' a = I_el Y

proof end;

theorem :: BVFUNC25:21

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds ((a 'imp' b) '&' a) 'imp' b = I_el Y

proof end;

theorem Th22: :: BVFUNC25:22

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds a 'imp' (('not' a) 'imp' a) = I_el Y

proof end;

theorem :: BVFUNC25:23

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds (('not' a) 'imp' a) 'eqv' a = I_el Y

proof end;

theorem :: BVFUNC25:24

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a 'or' (a 'imp' b) = I_el Y

proof end;

theorem :: BVFUNC25:25

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (a 'imp' b) 'or' (c 'imp' a) = I_el Y

proof end;

theorem :: BVFUNC25:26

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds (a 'imp' b) 'or' (('not' a) 'imp' b) = I_el Y

proof end;

theorem :: BVFUNC25:27

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds (a 'imp' b) 'or' (a 'imp' ('not' b)) = I_el Y

proof end;

theorem :: BVFUNC25:28

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds ('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = I_el Y

proof end;

theorem :: BVFUNC25:29

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = I_el Y

proof end;

theorem :: BVFUNC25:30

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a 'imp' b = a 'eqv' (a '&' b)

proof end;

theorem :: BVFUNC25:31

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds
( ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) iff a = b )

proof end;

theorem :: BVFUNC25:32

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds a = ('not' a) 'imp' a

proof end;

theorem Th33: :: BVFUNC25:33

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a 'imp' ((a 'imp' b) 'imp' a) = I_el Y

proof end;

theorem :: BVFUNC25:34

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a = (a 'imp' b) 'imp' a

proof end;

theorem :: BVFUNC25:35

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a = (b 'imp' a) '&' (('not' b) 'imp' a)

proof end;

theorem :: BVFUNC25:36

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a '&' b = 'not' (a 'imp' ('not' b))

proof end;

theorem :: BVFUNC25:37

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a 'or' b = ('not' a) 'imp' b

proof end;

theorem :: BVFUNC25:38

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a 'or' b = (a 'imp' b) 'imp' b

proof end;

theorem :: BVFUNC25:39

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds (a 'imp' b) 'imp' (a 'imp' a) = I_el Y

proof end;

theorem :: BVFUNC25:40

for Y being non empty set
for a, b, c, d being Element of Funcs Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = I_el Y

proof end;

theorem :: BVFUNC25:41

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (((a 'imp' b) '&' a) '&' c) 'imp' b = I_el Y

proof end;

theorem :: BVFUNC25:42

for Y being non empty set
for b, c, a being Element of Funcs Y,BOOLEAN holds (b 'imp' c) 'imp' ((a '&' b) 'imp' c) = I_el Y

proof end;

theorem :: BVFUNC25:43

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = I_el Y

proof end;

theorem :: BVFUNC25:44

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el Y

proof end;

theorem :: BVFUNC25:45

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds ((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c) = I_el Y

proof end;

theorem :: BVFUNC25:46

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (a '&' (a 'imp' b)) '&' (b 'imp' c) '<' c

proof end;

theorem :: BVFUNC25:47

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds ((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c) '<' ('not' a) 'imp' (b 'or' c)

proof end;