:: by Shunichi Kobayashi

::

:: Received April 23, 1999

:: Copyright (c) 1999-2012 Association of Mizar Users

begin

theorem :: BVFUNC_7:1

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (('not' a) 'imp' b) = b

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

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

for a, b, c being Function of 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 Function of Y,BOOLEAN holds a 'imp' (b '&' c) = (a 'imp' b) '&' (a 'imp' c)

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

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

for a, b, c being Function of 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 Function of Y,BOOLEAN holds (a '&' b) 'imp' c = a 'imp' (b 'imp' c)

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

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

for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'or' c) = (a '&' ('not' b)) 'imp' c

proof end;

theorem :: BVFUNC_7:11

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' ('not' b) = ('not' a) '&' ('not' b)

for a, b being Function of 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 Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) = ((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)

for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) = ((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)

proof end;

theorem :: BVFUNC_7:18

for Y being non empty set

for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (c 'imp' a) 'imp' (c 'imp' b)

for a, b, c being Function of 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 Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'eqv' c) 'eqv' (b 'eqv' c)

for a, b, c being Function of 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 Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'imp' c) 'eqv' (b 'imp' c)

for a, b, c being Function of 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 Function of Y,BOOLEAN holds a 'eqv' b '<' (c 'imp' a) 'eqv' (c 'imp' b)

for a, b, c being Function of 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 Function of Y,BOOLEAN holds a 'eqv' b '<' (a '&' c) 'eqv' (b '&' c)

for a, b, c being Function of 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 Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'or' c) 'eqv' (b 'or' c)

for a, b, c being Function of 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 Function of Y,BOOLEAN holds a '<' ((a 'eqv' b) 'eqv' (b 'eqv' a)) 'eqv' a

for a, b being Function of Y,BOOLEAN holds a '<' ((a 'eqv' b) 'eqv' (b 'eqv' a)) 'eqv' a

proof end;

theorem :: BVFUNC_7:27

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a '<' ((a '&' b) 'eqv' (b '&' a)) 'eqv' a

for a, b being Function of Y,BOOLEAN holds a '<' ((a '&' b) 'eqv' (b '&' a)) 'eqv' a

proof end;