:: BVFUNC_7 semantic presentation

theorem Th1: :: BVFUNC_7:1

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

proof end;

theorem Th2: :: BVFUNC_7:2

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

proof end;

theorem Th3: :: BVFUNC_7:3

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

proof end;

theorem Th4: :: BVFUNC_7:4

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

proof end;

theorem Th5: :: BVFUNC_7:5

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

proof end;

theorem Th6: :: BVFUNC_7:6

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

proof end;

theorem Th7: :: BVFUNC_7:7

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

proof end;

theorem Th8: :: BVFUNC_7:8

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

proof end;

theorem Th9: :: BVFUNC_7:9

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

proof end;

theorem Th10: :: BVFUNC_7:10

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

proof end;

theorem Th11: :: BVFUNC_7:11

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

proof end;

theorem Th12: :: BVFUNC_7:12

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

proof end;

theorem Th13: :: BVFUNC_7:13

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

proof end;

theorem Th14: :: BVFUNC_7:14

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

proof end;

theorem Th15: :: BVFUNC_7:15

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

proof end;

theorem Th16: :: BVFUNC_7:16

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

proof end;

theorem Th17: :: BVFUNC_7:17

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

proof end;

theorem Th18: :: BVFUNC_7:18

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₄ 'imp' b₃)

proof end;

theorem Th19: :: BVFUNC_7:19

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'eqv' b₃ '<' (b₂ 'eqv' b₄) 'eqv' (b₃ 'eqv' b₄)

proof end;

theorem Th20: :: BVFUNC_7:20

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

proof end;

theorem Th21: :: BVFUNC_7:21

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

proof end;

theorem Th22: :: BVFUNC_7:22

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

proof end;

theorem Th23: :: BVFUNC_7:23

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

proof end;

theorem Th24: :: BVFUNC_7:24

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

proof end;

theorem Th25: :: BVFUNC_7:25

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

proof end;

theorem Th26: :: BVFUNC_7:26

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

proof end;

theorem Th27: :: BVFUNC_7:27

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ '<' ((b₂ '&' b₃) 'eqv' (b₃ '&' b₂)) 'eqv' b₂

proof end;