:: Propositional Calculus for Boolean Valued Functions, {VII }
:: by Shunichi Kobayashi
::
:: Received February 6, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

theorem :: BVFUNC25:1
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'imp' b) = a '&' ('not' b)
proofend;

theorem Th2: :: BVFUNC25:2
for Y being non empty set
for b, a being Function of Y,BOOLEAN holds (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y
proofend;

theorem Th3: :: BVFUNC25:3
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' b = ('not' b) 'imp' ('not' a)
proofend;

theorem :: BVFUNC25:4
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = ('not' a) 'eqv' ('not' b)
proofend;

theorem Th5: :: BVFUNC25:5
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' b = a 'imp' (a '&' b)
proofend;

theorem :: BVFUNC25:6
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'or' b) 'imp' (a '&' b)
proofend;

theorem :: BVFUNC25:7
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'eqv' ('not' a) = O_el Y
proofend;

theorem :: BVFUNC25:8
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'imp' c) = b 'imp' (a 'imp' c)
proofend;

theorem :: BVFUNC25:9
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'imp' c) = (a 'imp' b) 'imp' (a 'imp' c)
proofend;

theorem :: BVFUNC25:10
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = a 'xor' ('not' b)
proofend;

theorem :: BVFUNC25:11
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a '&' (b 'xor' c) = (a '&' b) 'xor' (a '&' c)
proofend;

theorem :: BVFUNC25:12
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = 'not' (a 'xor' b)
proofend;

theorem :: BVFUNC25:13
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' a = O_el Y
proofend;

theorem :: BVFUNC25:14
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' ('not' a) = I_el Y
proofend;

theorem :: BVFUNC25:15
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a
proofend;

theorem Th16: :: BVFUNC25:16
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b))
proofend;

theorem Th17: :: BVFUNC25:17
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'or' (('not' a) '&' ('not' b)) = (('not' a) 'or' b) '&' (a 'or' ('not' b))
proofend;

theorem :: BVFUNC25:18
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c
proofend;

theorem :: BVFUNC25:19
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'eqv' (b 'eqv' c) = (a 'eqv' b) 'eqv' c
proofend;

theorem :: BVFUNC25:20
for Y being non empty set
for a being Function of Y,BOOLEAN holds ('not' ('not' a)) 'imp' a = I_el Y by BVFUNC_5:7;

theorem :: BVFUNC25:21
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ((a 'imp' b) '&' a) 'imp' b = I_el Y
proofend;

theorem Th22: :: BVFUNC25:22
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (('not' a) 'imp' a) = I_el Y
proofend;

theorem :: BVFUNC25:23
for Y being non empty set
for a being Function of Y,BOOLEAN holds (('not' a) 'imp' a) 'eqv' a = I_el Y
proofend;

theorem :: BVFUNC25:24
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' (a 'imp' b) = I_el Y
proofend;

theorem :: BVFUNC25:25
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (c 'imp' a) = I_el Y
proofend;

theorem :: BVFUNC25:26
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (('not' a) 'imp' b) = I_el Y
proofend;

theorem :: BVFUNC25:27
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (a 'imp' ('not' b)) = I_el Y
proofend;

theorem :: BVFUNC25:28
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = I_el Y
proofend;

theorem :: BVFUNC25:29
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = I_el Y
proofend;

theorem :: BVFUNC25:30
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' b = a 'eqv' (a '&' b)
proofend;

theorem :: BVFUNC25:31
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) iff a = b )
proofend;

theorem :: BVFUNC25:32
for Y being non empty set
for a being Function of Y,BOOLEAN holds a = ('not' a) 'imp' a
proofend;

theorem Th33: :: BVFUNC25:33
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' ((a 'imp' b) 'imp' a) = I_el Y
proofend;

theorem :: BVFUNC25:34
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (a 'imp' b) 'imp' a
proofend;

theorem :: BVFUNC25:35
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (b 'imp' a) '&' (('not' b) 'imp' a)
proofend;

theorem :: BVFUNC25:36
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b = 'not' (a 'imp' ('not' b))
proofend;

theorem :: BVFUNC25:37
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' b = ('not' a) 'imp' b
proofend;

theorem :: BVFUNC25:38
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' b = (a 'imp' b) 'imp' b
proofend;

theorem :: BVFUNC25:39
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (a 'imp' a) = I_el Y
proofend;

theorem :: BVFUNC25:40
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = I_el Y
proofend;

theorem :: BVFUNC25:41
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((a 'imp' b) '&' a) '&' c) 'imp' b = I_el Y
proofend;

theorem :: BVFUNC25:42
for Y being non empty set
for b, c, a being Function of Y,BOOLEAN holds (b 'imp' c) 'imp' ((a '&' b) 'imp' c) = I_el Y
proofend;

theorem :: BVFUNC25:43
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = I_el Y
proofend;

theorem :: BVFUNC25:44
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el Y
proofend;

theorem :: BVFUNC25:45
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c) = I_el Y
proofend;

theorem :: BVFUNC25:46
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&amp;' (a 'imp' b)) '&amp;' (b 'imp' c) '<' c
proofend;

theorem :: BVFUNC25:47
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) '&amp;' (a 'imp' c)) '&amp;' (b 'imp' c) '<' ('not' a) 'imp' (b 'or' c)
proofend;