for b₁, b₂, b₃ being boolean set holds
( b₁ 'or' (b₂ 'nor' b₃) = (b₁ 'or' ('not' b₂)) '&' (b₁ 'or' ('not' b₃)) & b₁ 'or' (b₂ 'nor' b₃) = (b₂ 'imp' b₁) '&' (b₃ 'imp' b₁) )

proof end;

theorem Th25: :: BINARI_6:25

for b₁, b₂ being boolean set holds b₁ 'or' (b₁ 'or' b₂) = b₁ 'or' b₂

proof end;

theorem Th26: :: BINARI_6:26

for b₁, b₂ being boolean set holds b₁ 'or' (b₁ 'imp' b₂) = TRUE

proof end;

theorem Th27: :: BINARI_6:27

for b₁, b₂ being boolean set holds b₁ 'or' (b₁ 'eqv' b₂) = b₂ 'imp' b₁

proof end;

theorem Th28: :: BINARI_6:28

for b₁, b₂ being boolean set holds b₁ 'or' (b₁ 'nand' b₂) = TRUE

proof end;

theorem Th29: :: BINARI_6:29

for b₁, b₂ being boolean set holds b₁ 'or' (b₁ 'nor' b₂) = b₂ 'imp' b₁

proof end;

theorem Th30: :: BINARI_6:30

for b₁, b₂, b₃ being boolean set holds b₁ 'imp' (b₂ 'xor' b₃) = (('not' b₁) 'or' (('not' b₂) '&' b₃)) 'or' (b₂ '&' ('not' b₃))

proof end;

theorem Th31: :: BINARI_6:31

for b₁, b₂, b₃ being boolean set holds b₁ 'imp' (b₂ 'eqv' b₃) = ((('not' b₁) 'or' ('not' b₂)) 'or' b₃) '&' ((('not' b₁) 'or' b₂) 'or' ('not' b₃))

proof end;

theorem Th32: :: BINARI_6:32

for b₁, b₂, b₃ being boolean set holds b₁ 'imp' (b₂ 'nand' b₃) = (('not' b₁) 'or' ('not' b₂)) 'or' ('not' b₃)

proof end;

theorem Th33: :: BINARI_6:33

for b₁, b₂, b₃ being boolean set holds
( b₁ 'imp' (b₂ 'nor' b₃) = (('not' b₁) 'or' ('not' b₂)) '&' (('not' b₁) 'or' ('not' b₃)) & b₁ 'imp' (b₂ 'nor' b₃) = (b₁ 'imp' ('not' b₂)) '&' (b₁ 'imp' ('not' b₃)) )

proof end;

theorem Th34: :: BINARI_6:34

for b₁, b₂ being boolean set holds b₁ 'imp' (b₁ '&' b₂) = b₁ 'imp' b₂

proof end;

theorem Th35: :: BINARI_6:35

for b₁, b₂ being boolean set holds b₁ 'imp' (b₁ 'or' b₂) = TRUE

proof end;

theorem Th36: :: BINARI_6:36

for b₁, b₂ being boolean set holds b₁ 'imp' (b₁ 'xor' b₂) = ('not' b₁) 'or' ('not' b₂)

proof end;

theorem Th37: :: BINARI_6:37

for b₁, b₂ being boolean set holds b₁ 'imp' (b₁ 'imp' b₂) = b₁ 'imp' b₂

proof end;

theorem Th38: :: BINARI_6:38

for b₁, b₂ being boolean set holds
( b₁ 'imp' (b₁ 'eqv' b₂) = b₁ 'imp' b₂ & b₁ 'imp' (b₁ 'eqv' b₂) = b₁ 'imp' (b₁ 'imp' b₂) )

proof end;

theorem Th39: :: BINARI_6:39

for b₁, b₂ being boolean set holds b₁ 'imp' (b₁ 'nand' b₂) = 'not' (b₁ '&' b₂)

proof end;

theorem Th40: :: BINARI_6:40

for b₁, b₂ being boolean set holds b₁ 'imp' (b₁ 'nor' b₂) = 'not' b₁

proof end;

theorem Th41: :: BINARI_6:41

for b₁, b₂, b₃ being boolean set holds
( b₁ 'nand' (b₂ 'imp' b₃) = (('not' b₁) 'or' b₂) '&' (('not' b₁) 'or' ('not' b₃)) & b₁ 'nand' (b₂ 'imp' b₃) = (b₁ 'imp' b₂) '&' (b₁ 'imp' ('not' b₃)) )

proof end;

theorem Th42: :: BINARI_6:42

for b₁, b₂, b₃ being boolean set holds b₁ 'nand' (b₂ 'eqv' b₃) = 'not' ((b₁ '&' (('not' b₂) 'or' b₃)) '&' (('not' b₃) 'or' b₂))

proof end;

theorem Th43: :: BINARI_6:43

for b₁, b₂, b₃ being boolean set holds
( b₁ 'nand' (b₂ 'nand' b₃) = (('not' b₁) 'or' b₂) '&' (('not' b₁) 'or' b₃) & b₁ 'nand' (b₂ 'nand' b₃) = (b₁ 'imp' b₂) '&' (b₁ 'imp' b₃) )

proof end;

theorem Th44: :: BINARI_6:44

for b₁, b₂, b₃ being boolean set holds b₁ 'nand' (b₂ 'nor' b₃) = (('not' b₁) 'or' b₂) 'or' b₃

proof end;

theorem Th45: :: BINARI_6:45

for b₁, b₂ being boolean set holds b₁ 'nand' (b₁ '&' b₂) = 'not' (b₁ '&' b₂)

proof end;

theorem Th46: :: BINARI_6:46

for b₁, b₂ being boolean set holds b₁ 'nand' (b₁ 'xor' b₂) = b₁ 'imp' b₂

proof end;

theorem Th47: :: BINARI_6:47

for b₁, b₂ being boolean set holds b₁ 'nand' (b₁ 'imp' b₂) = 'not' (b₁ '&' b₂)

proof end;

theorem Th48: :: BINARI_6:48

for b₁, b₂ being boolean set holds b₁ 'nand' (b₁ 'eqv' b₂) = 'not' (b₁ '&' b₂)

proof end;

theorem Th49: :: BINARI_6:49

for b₁, b₂ being boolean set holds b₁ 'nand' (b₁ 'nand' b₂) = b₁ 'imp' b₂

proof end;

theorem Th50: :: BINARI_6:50

for b₁, b₂ being boolean set holds b₁ 'nand' (b₁ 'nor' b₂) = TRUE

proof end;

theorem Th51: :: BINARI_6:51

for b₁, b₂, b₃ being boolean set holds b₁ 'nor' (b₂ 'xor' b₃) = 'not' ((b₁ 'or' (('not' b₂) '&' b₃)) 'or' (b₂ '&' ('not' b₃)))

proof end;

theorem Th52: :: BINARI_6:52

for b₁, b₂, b₃ being boolean set holds b₁ 'nor' (b₂ 'eqv' b₃) = 'not' (((b₁ 'or' ('not' b₂)) 'or' b₃) '&' ((b₁ 'or' ('not' b₃)) 'or' b₂))

proof end;

theorem Th53: :: BINARI_6:53

for b₁, b₂, b₃ being boolean set holds b₁ 'nor' (b₂ 'nand' b₃) = (('not' b₁) '&' b₂) '&' b₃

proof end;

theorem Th54: :: BINARI_6:54

for b₁, b₂, b₃ being boolean set holds b₁ 'nor' (b₂ 'nor' b₃) = (('not' b₁) '&' b₂) 'or' (('not' b₁) '&' b₃)

proof end;

theorem Th55: :: BINARI_6:55

for b₁, b₂ being boolean set holds b₁ 'nor' (b₁ '&' b₂) = 'not' b₁

proof end;

theorem Th56: :: BINARI_6:56

for b₁, b₂ being boolean set holds b₁ 'nor' (b₁ 'or' b₂) = ('not' b₁) '&' ('not' b₂)

proof end;

theorem Th57: :: BINARI_6:57

for b₁, b₂ being boolean set holds b₁ 'nor' (b₁ 'xor' b₂) = ('not' b₁) '&' ('not' b₂)

proof end;

theorem Th58: :: BINARI_6:58

for b₁, b₂ being boolean set holds b₁ 'nor' (b₁ 'imp' b₂) = FALSE

proof end;

theorem Th59: :: BINARI_6:59

for b₁, b₂ being boolean set holds b₁ 'nor' (b₁ 'eqv' b₂) = ('not' b₁) '&' b₂

proof end;

theorem Th60: :: BINARI_6:60

for b₁, b₂ being boolean set holds b₁ 'nor' (b₁ 'nand' b₂) = FALSE

proof end;

theorem Th61: :: BINARI_6:61

for b₁, b₂ being boolean set holds b₁ 'nor' (b₁ 'nor' b₂) = ('not' b₁) '&' b₂

proof end;

theorem Th62: :: BINARI_6:62

for b₁, b₂, b₃ being boolean set holds b₁ 'xor' (b₂ '&' b₃) = (b₁ 'or' (b₂ '&' b₃)) '&' (('not' b₁) 'or' ('not' (b₂ '&' b₃)))

proof end;

theorem Th63: :: BINARI_6:63

for b₁, b₂ being boolean set holds b₁ 'xor' (b₁ '&' b₂) = b₁ '&' ('not' b₂)

proof end;

theorem Th64: :: BINARI_6:64

for b₁, b₂ being boolean set holds b₁ 'xor' (b₁ 'or' b₂) = ('not' b₁) '&' b₂

proof end;

theorem Th65: :: BINARI_6:65

for b₁, b₂ being boolean set holds ('not' b₁) '&' (b₁ 'xor' b₂) = ('not' b₁) '&' b₂

proof end;

theorem Th66: :: BINARI_6:66

for b₁, b₂ being boolean set holds b₁ '&' ('not' (b₁ 'xor' b₂)) = b₁ '&' b₂

proof end;

theorem Th67: :: BINARI_6:67

for b₁, b₂ being boolean set holds b₁ 'xor' (b₁ 'xor' b₂) = b₂

proof end;

theorem Th68: :: BINARI_6:68

for b₁, b₂ being boolean set holds b₁ '&' ('not' (b₁ 'imp' b₂)) = b₁ '&' ('not' b₂)

proof end;

theorem Th69: :: BINARI_6:69

for b₁, b₂ being boolean set holds b₁ 'xor' (b₁ 'imp' b₂) = ('not' b₁) 'or' ('not' b₂)

proof end;

theorem Th70: :: BINARI_6:70

for b₁, b₂ being boolean set holds ('not' b₁) '&' (b₁ 'eqv' b₂) = ('not' b₁) '&' ('not' b₂)

proof end;

theorem Th71: :: BINARI_6:71

for b₁, b₂ being boolean set holds b₁ '&' ('not' (b₁ 'eqv' b₂)) = b₁ '&' ('not' b₂)

proof end;

theorem Th72: :: BINARI_6:72

for b₁, b₂ being boolean set holds b₁ 'xor' (b₁ 'eqv' b₂) = 'not' b₂

proof end;

theorem Th73: :: BINARI_6:73

for b₁, b₂ being boolean set holds b₁ 'xor' (b₁ 'nand' b₂) = b₁ 'imp' b₂

proof end;

theorem Th74: :: BINARI_6:74

for b₁, b₂ being boolean set holds b₁ 'xor' (b₁ 'nor' b₂) = b₂ 'imp' b₁

proof end;

theorem Th75: :: BINARI_6:75

for b₁, b₂ being boolean set holds ('not' b₁) '&' (b₁ 'imp' b₂) = ('not' b₁) 'or' (('not' b₁) '&' b₂)

proof end;

theorem Th76: :: BINARI_6:76

for b₁, b₂, b₃ being boolean set holds ('not' b₁) '&' (b₂ 'eqv' b₃) = (('not' b₁) '&' (('not' b₂) 'or' b₃)) '&' (('not' b₃) 'or' b₂)

proof end;

theorem Th77: :: BINARI_6:77

for b₁, b₂ being boolean set holds ('not' b₁) '&' (b₁ 'eqv' b₂) = (('not' b₁) '&' ('not' b₂)) '&' (('not' b₁) 'or' b₂)

proof end;

theorem Th78: :: BINARI_6:78

for b₁, b₂ being boolean set holds ('not' b₁) '&' (b₁ 'nand' b₂) = ('not' b₁) 'or' (('not' b₁) '&' ('not' b₂))

proof end;

theorem Th79: :: BINARI_6:79

for b₁, b₂ being boolean set holds ('not' b₁) '&' (b₁ 'nor' b₂) = ('not' b₁) '&' ('not' b₂)

proof end;

theorem Th80: :: BINARI_6:80

for b₁, b₂ being boolean set holds ('not' b₁) 'or' (b₁ 'imp' b₂) = ('not' b₁) 'or' b₂

proof end;

theorem Th81: :: BINARI_6:81

for b₁, b₂ being boolean set holds ('not' b₁) 'or' (b₁ 'eqv' b₂) = ('not' b₁) 'or' b₂

proof end;

theorem Th82: :: BINARI_6:82

for b₁, b₂ being boolean set holds ('not' b₁) 'or' (b₁ 'nand' b₂) = ('not' b₁) 'or' ('not' b₂)

proof end;

theorem Th83: :: BINARI_6:83

for b₁, b₂ being boolean set holds ('not' b₁) 'xor' (b₁ 'imp' b₂) = b₁ '&' b₂

proof end;

theorem Th84: :: BINARI_6:84

for b₁, b₂ being boolean set holds ('not' b₁) 'xor' (b₂ 'imp' b₁) = (b₁ '&' (b₁ 'or' ('not' b₂))) 'or' (('not' b₁) '&' b₂)

proof end;

theorem Th85: :: BINARI_6:85

for b₁, b₂ being boolean set holds 'not' (b₁ 'imp' b₂) = b₁ '&' ('not' b₂)

proof end;

theorem Th86: :: BINARI_6:86

for b₁, b₂ being boolean set holds 'not' (b₁ 'eqv' b₂) = (b₁ '&' ('not' b₂)) 'or' (b₂ '&' ('not' b₁))

proof end;

theorem Th87: :: BINARI_6:87

for b₁, b₂ being boolean set holds ('not' b₁) 'xor' (b₁ 'eqv' b₂) = b₂

proof end;