The abstract of the Mizar article:

Propositional Calculus for Boolean Valued Functions. Part III

by

Shunichi Kobayashi

Received April 23, 1999

MML identifier: BVFUNC_7

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_2, MARGREL1, BVFUNC_1, ZF_LANG, FUNCT_1, RELAT_1, PARTIT1;
 notation TARSKI, XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, RELAT_1, FUNCT_1,
      FRAENKEL, BINARITH, BVFUNC_1;
 constructors BINARITH, BVFUNC_1;
 clusters MARGREL1, VALUAT_1, BINARITH, FRAENKEL;
 requirements SUBSET, BOOLE;


begin

::Chap. 1  Propositional Calculus

reserve Y for non empty set;

theorem :: BVFUNC_7:1
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' ('not' a 'imp' b) = b;

theorem :: BVFUNC_7:2
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (a 'imp' 'not' b) = 'not' a;

theorem :: BVFUNC_7:3
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
a 'imp' (b 'or' c) = (a 'imp' b) 'or' (a 'imp' c);

theorem :: BVFUNC_7:4
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
a 'imp' (b '&' c) = (a 'imp' b) '&' (a 'imp' c);

theorem :: BVFUNC_7:5
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'or' b) 'imp' c = (a 'imp' c) '&' (b 'imp' c);

theorem :: BVFUNC_7:6
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a '&' b) 'imp' c = (a 'imp' c) 'or' (b 'imp' c);

theorem :: BVFUNC_7:7
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a '&' b) 'imp' c = a 'imp' (b 'imp' c);

theorem :: BVFUNC_7:8
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a '&' b) 'imp' c = a 'imp' ('not' b 'or' c);

theorem :: BVFUNC_7:9
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
a 'imp' (b 'or' c) = (a '&' 'not' b) 'imp' c;

theorem :: BVFUNC_7:10
for a,b being Element of Funcs(Y,BOOLEAN) holds
a '&' (a 'imp' b) = a '&' b;

theorem :: BVFUNC_7:11
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' 'not' b = 'not' a '&' 'not' b;

theorem :: BVFUNC_7:12
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);

theorem :: BVFUNC_7:13
for a being Element of Funcs(Y,BOOLEAN) holds
I_el(Y) 'imp' a = a;

theorem :: BVFUNC_7:14
for a being Element of Funcs(Y,BOOLEAN) holds
a 'imp' O_el(Y) = 'not' a;

theorem :: BVFUNC_7:15
for a being Element of Funcs(Y,BOOLEAN) holds
O_el(Y) 'imp' a = I_el(Y);

theorem :: BVFUNC_7:16
for a being Element of Funcs(Y,BOOLEAN) holds
a 'imp' I_el(Y) = I_el(Y);

theorem :: BVFUNC_7:17
for a being Element of Funcs(Y,BOOLEAN) holds
a 'imp' 'not' a = 'not' a;

theorem :: BVFUNC_7:18
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '<' (c 'imp' a) 'imp' (c 'imp' b);

theorem :: BVFUNC_7:19
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b) '<' (a 'eqv' c) 'eqv' (b 'eqv' c);

theorem :: BVFUNC_7:20
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b) '<' (a 'imp' c) 'eqv' (b 'imp' c);

theorem :: BVFUNC_7:21
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b) '<' (c 'imp' a) 'eqv' (c 'imp' b);

theorem :: BVFUNC_7:22
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b) '<' (a '&' c) 'eqv' (b '&' c);

theorem :: BVFUNC_7:23
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b) '<' (a 'or' c) 'eqv' (b 'or' c);

theorem :: BVFUNC_7:24
for a,b being Element of Funcs(Y,BOOLEAN) holds
a '<' (a 'eqv' b) 'eqv' (b 'eqv' a) 'eqv' a;

theorem :: BVFUNC_7:25
for a,b being Element of Funcs(Y,BOOLEAN) holds
a '<' (a 'imp' b) 'eqv' b;

theorem :: BVFUNC_7:26
for a,b being Element of Funcs(Y,BOOLEAN) holds
a '<' (b 'imp' a) 'eqv' a;

theorem :: BVFUNC_7:27
for a,b being Element of Funcs(Y,BOOLEAN) holds
a '<' (a '&' b) 'eqv' (b '&' a) 'eqv' a;