:: Propositional Calculus for Boolean Valued Functions, II
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received March 13, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

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

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

theorem :: BVFUNC_6:3
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'or' b) 'eqv' (b 'or' a) = I_el Y
proofend;

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

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

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

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

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

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

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

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

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

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

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

theorem :: BVFUNC_6:15
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a '&' b = I_el Y holds
a 'or' b = I_el Y
proofend;

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

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

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

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

theorem :: BVFUNC_6:20
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a 'or' b = I_el Y & 'not' a = I_el Y holds
b = I_el Y
proofend;

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

theorem :: BVFUNC_6:22
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'imp' b = I_el Y & c 'imp' d = I_el Y holds
(a 'or' c) 'imp' (b 'or' d) = I_el Y
proofend;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: BVFUNC_6:43
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'eqv' b) 'imp' (b 'imp' a) = I_el Y by Th42;

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

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

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