:: Propositional Calculus For Boolean Valued Functions, III
:: 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
proofend;

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
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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

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)
proofend;

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)
proofend;

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

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

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

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

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

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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

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)
proofend;

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
proofend;

theorem :: BVFUNC_7:25
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' (a 'imp' b) 'eqv' b
proofend;

theorem :: BVFUNC_7:26
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' (b 'imp' a) 'eqv' a
proofend;

theorem :: BVFUNC_7:27
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' ((a '&amp;' b) 'eqv' (b '&amp;' a)) 'eqv' a
proofend;