:: BVFUNC_6 semantic presentation

theorem Th1: :: BVFUNC_6:1

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'imp' (b₃ 'imp' (b₂ '&' b₃)) = I_el b₁

proof end;

theorem Th2: :: BVFUNC_6:2

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₃) 'imp' ((b₃ 'imp' b₂) 'imp' (b₂ 'eqv' b₃)) = I_el b₁

proof end;

theorem Th3: :: BVFUNC_6:3

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (b₂ 'or' b₃) 'eqv' (b₃ 'or' b₂) = I_el b₁

proof end;

theorem Th4: :: BVFUNC_6:4

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ '&' b₃) 'imp' b₄) 'imp' (b₂ 'imp' (b₃ 'imp' b₄)) = I_el b₁

proof end;

theorem Th5: :: BVFUNC_6:5

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' (b₃ 'imp' b₄)) 'imp' ((b₂ '&' b₃) 'imp' b₄) = I_el b₁

proof end;

theorem Th6: :: BVFUNC_6:6

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₄ 'imp' b₂) 'imp' ((b₄ 'imp' b₃) 'imp' (b₄ 'imp' (b₂ '&' b₃))) = I_el b₁

proof end;

theorem Th7: :: BVFUNC_6:7

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ 'or' b₃) 'imp' b₄) 'imp' ((b₂ 'imp' b₄) 'or' (b₃ 'imp' b₄)) = I_el b₁

proof end;

theorem Th8: :: BVFUNC_6:8

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₄) 'imp' ((b₃ 'imp' b₄) 'imp' ((b₂ 'or' b₃) 'imp' b₄)) = I_el b₁

proof end;

theorem Th9: :: BVFUNC_6:9

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ 'imp' b₄) '&' (b₃ 'imp' b₄)) 'imp' ((b₂ 'or' b₃) 'imp' b₄) = I_el b₁

proof end;

theorem Th10: :: BVFUNC_6:10

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' (b₃ '&' ('not' b₃))) 'imp' ('not' b₂) = I_el b₁

proof end;

theorem Th11: :: BVFUNC_6:11

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ 'or' b₃) '&' (b₂ 'or' b₄)) 'imp' (b₂ 'or' (b₃ '&' b₄)) = I_el b₁

proof end;

theorem Th12: :: BVFUNC_6:12

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ '&' (b₃ 'or' b₄)) 'imp' ((b₂ '&' b₃) 'or' (b₂ '&' b₄)) = I_el b₁

proof end;

theorem Th13: :: BVFUNC_6:13

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ 'or' b₄) '&' (b₃ 'or' b₄)) 'imp' ((b₂ '&' b₃) 'or' b₄) = I_el b₁

proof end;

theorem Th14: :: BVFUNC_6:14

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ 'or' b₃) '&' b₄) 'imp' ((b₂ '&' b₄) 'or' (b₃ '&' b₄)) = I_el b₁

proof end;

theorem Th15: :: BVFUNC_6:15

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN st b₂ '&' b₃ = I_el b₁ holds
b₂ 'or' b₃ = I_el b₁

proof end;

theorem Th16: :: BVFUNC_6:16

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN st b₂ 'imp' b₃ = I_el b₁ holds
(b₂ 'or' b₄) 'imp' (b₃ 'or' b₄) = I_el b₁

proof end;

theorem Th17: :: BVFUNC_6:17

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN st b₂ 'imp' b₃ = I_el b₁ holds
(b₂ '&' b₄) 'imp' (b₃ '&' b₄) = I_el b₁

proof end;

theorem Th18: :: BVFUNC_6:18

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN st b₄ 'imp' b₂ = I_el b₁ & b₄ 'imp' b₃ = I_el b₁ holds
b₄ 'imp' (b₂ '&' b₃) = I_el b₁

proof end;

theorem Th19: :: BVFUNC_6:19

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN st b₂ 'imp' b₄ = I_el b₁ & b₃ 'imp' b₄ = I_el b₁ holds
(b₂ 'or' b₃) 'imp' b₄ = I_el b₁

proof end;

theorem Th20: :: BVFUNC_6:20

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN st b₂ 'or' b₃ = I_el b₁ & 'not' b₂ = I_el b₁ holds
b₃ = I_el b₁

proof end;

theorem Th21: :: BVFUNC_6:21

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of Funcs b₁,BOOLEAN st b₂ 'imp' b₃ = I_el b₁ & b₄ 'imp' b₅ = I_el b₁ holds
(b₂ '&' b₄) 'imp' (b₃ '&' b₅) = I_el b₁

proof end;

theorem Th22: :: BVFUNC_6:22

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of Funcs b₁,BOOLEAN st b₂ 'imp' b₃ = I_el b₁ & b₄ 'imp' b₅ = I_el b₁ holds
(b₂ 'or' b₄) 'imp' (b₃ 'or' b₅) = I_el b₁

proof end;

theorem Th23: :: BVFUNC_6:23

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN st (b₂ '&' ('not' b₃)) 'imp' ('not' b₂) = I_el b₁ holds
b₂ 'imp' b₃ = I_el b₁

proof end;

theorem Th24: :: BVFUNC_6:24

canceled;

theorem Th25: :: BVFUNC_6:25

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN st b₂ 'imp' ('not' b₃) = I_el b₁ holds
b₃ 'imp' ('not' b₂) = I_el b₁

proof end;

theorem Th26: :: BVFUNC_6:26

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN st ('not' b₂) 'imp' b₃ = I_el b₁ holds
('not' b₃) 'imp' b₂ = I_el b₁

proof end;

theorem Th27: :: BVFUNC_6:27

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'imp' (b₂ 'or' b₃) = I_el b₁

proof end;

theorem Th28: :: BVFUNC_6:28

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (b₂ 'or' b₃) 'imp' (('not' b₂) 'imp' b₃) = I_el b₁

proof end;

theorem Th29: :: BVFUNC_6:29

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds ('not' (b₂ 'or' b₃)) 'imp' (('not' b₂) '&' ('not' b₃)) = I_el b₁

proof end;

theorem Th30: :: BVFUNC_6:30

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (('not' b₂) '&' ('not' b₃)) 'imp' ('not' (b₂ 'or' b₃)) = I_el b₁

proof end;

theorem Th31: :: BVFUNC_6:31

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds ('not' (b₂ 'or' b₃)) 'imp' ('not' b₂) = I_el b₁

proof end;

theorem Th32: :: BVFUNC_6:32

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds (b₂ 'or' b₂) 'imp' b₂ = I_el b₁

proof end;

theorem Th33: :: BVFUNC_6:33

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (b₂ '&' ('not' b₂)) 'imp' b₃ = I_el b₁

proof end;

theorem Th34: :: BVFUNC_6:34

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₃) 'imp' (('not' b₂) 'or' b₃) = I_el b₁

proof end;

theorem Th35: :: BVFUNC_6:35

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (b₂ '&' b₃) 'imp' ('not' (b₂ 'imp' ('not' b₃))) = I_el b₁

proof end;

theorem Th36: :: BVFUNC_6:36

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds ('not' (b₂ 'imp' ('not' b₃))) 'imp' (b₂ '&' b₃) = I_el b₁

proof end;

theorem Th37: :: BVFUNC_6:37

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds ('not' (b₂ '&' b₃)) 'imp' (('not' b₂) 'or' ('not' b₃)) = I_el b₁

proof end;

theorem Th38: :: BVFUNC_6:38

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (('not' b₂) 'or' ('not' b₃)) 'imp' ('not' (b₂ '&' b₃)) = I_el b₁

proof end;

theorem Th39: :: BVFUNC_6:39

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (b₂ '&' b₃) 'imp' b₂ = I_el b₁

proof end;

theorem Th40: :: BVFUNC_6:40

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (b₂ '&' b₃) 'imp' (b₂ 'or' b₃) = I_el b₁

proof end;

theorem Th41: :: BVFUNC_6:41

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (b₂ '&' b₃) 'imp' b₃ = I_el b₁

proof end;

theorem Th42: :: BVFUNC_6:42

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds b₂ 'imp' (b₂ '&' b₂) = I_el b₁

proof end;

theorem Th43: :: BVFUNC_6:43

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (b₂ 'eqv' b₃) 'imp' (b₂ 'imp' b₃) = I_el b₁

proof end;

theorem Th44: :: BVFUNC_6:44

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds (b₂ 'eqv' b₃) 'imp' (b₃ 'imp' b₂) = I_el b₁

proof end;

theorem Th45: :: BVFUNC_6:45

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ 'or' b₃) 'or' b₄) 'imp' (b₂ 'or' (b₃ 'or' b₄)) = I_el b₁

proof end;

theorem Th46: :: BVFUNC_6:46

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ '&' b₃) '&' b₄) 'imp' (b₂ '&' (b₃ '&' b₄)) = I_el b₁

proof end;

theorem Th47: :: BVFUNC_6:47

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'or' (b₃ 'or' b₄)) 'imp' ((b₂ 'or' b₃) 'or' b₄) = I_el b₁

proof end;