:: Propositional Calculus For Boolean Valued Functions, III
:: by Shunichi Kobayashi
::
:: Received April 23, 1999
:: Copyright (c) 1999-2011 Association of Mizar Users


begin

theorem :: BVFUNC_7:1
for Y being non empty set
for a, b being Element of Funcs (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 Element of Funcs (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 Element of Funcs (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 Element of Funcs (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 Element of Funcs (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 Element of Funcs (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 Element of Funcs (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 Element of Funcs (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 Element of Funcs (Y,BOOLEAN) holds a 'imp' (b 'or' c) = (a '&' ('not' b)) 'imp' c
proof end;

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

theorem :: BVFUNC_7:11
for Y being non empty set
for a, b being Element of Funcs (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 Element of Funcs (Y,BOOLEAN) holds (a 'imp' b) '&' (b 'imp' c) = ((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)
proof end;

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

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

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

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

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

theorem :: BVFUNC_7:18
for Y being non empty set
for a, b, c being Element of Funcs (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 Element of Funcs (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 Element of Funcs (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 Element of Funcs (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 Element of Funcs (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 Element of Funcs (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 Element of Funcs (Y,BOOLEAN) holds a '<' ((a 'eqv' b) 'eqv' (b 'eqv' a)) 'eqv' a
proof end;

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

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

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