:: Propositional Calculus For Boolean Valued Functions, III
:: by Shunichi Kobayashi
::
:: Received April 23, 1999
:: Copyright (c) 1999-2011 Association of Mizar Users

begin

theorem :: BVFUNC_7:1

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

proof end;

theorem :: BVFUNC_7:2

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

proof end;

theorem :: BVFUNC_7:3

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

proof end;

theorem :: BVFUNC_7:4

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

proof end;

theorem :: BVFUNC_7:5

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

proof end;

theorem :: BVFUNC_7:6

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

proof end;

theorem Th7: :: BVFUNC_7:7

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

proof end;

theorem :: BVFUNC_7:8

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

proof end;

theorem :: BVFUNC_7:9

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

proof end;

theorem :: BVFUNC_7:10

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

proof end;

theorem :: BVFUNC_7:11

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

proof end;

theorem :: BVFUNC_7:12

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

proof end;

theorem :: BVFUNC_7:13

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

proof end;

theorem :: BVFUNC_7:14

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

proof end;

theorem :: BVFUNC_7:15

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

proof end;

theorem :: BVFUNC_7:16

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

proof end;

theorem :: BVFUNC_7:17

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

proof end;

theorem :: BVFUNC_7:18

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

proof end;

theorem :: BVFUNC_7:19

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

proof end;

theorem :: BVFUNC_7:20

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

proof end;

theorem :: BVFUNC_7:21

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

proof end;

theorem :: BVFUNC_7:22

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

proof end;

theorem :: BVFUNC_7:23

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

proof end;

theorem :: BVFUNC_7:24

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

proof end;

theorem :: BVFUNC_7:25

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

proof end;

theorem :: BVFUNC_7:26

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

proof end;

theorem :: BVFUNC_7:27

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

proof end;