:: PROCAL_1 semantic presentation

theorem Th1: :: PROCAL_1:1

for b₁ being Element of CQC-WFF holds 'not' (b₁ '&' ('not' b₁)) in TAUT

proof end;

Lemma2: for b₁, b₂ being Element of CQC-WFF holds b₁ 'or' b₂ = ('not' b₁) => b₂

proof end;

theorem Th2: :: PROCAL_1:2

for b₁ being Element of CQC-WFF holds b₁ 'or' ('not' b₁) in TAUT

proof end;

theorem Th3: :: PROCAL_1:3

for b₁, b₂ being Element of CQC-WFF holds b₁ => (b₁ 'or' b₂) in TAUT

proof end;

theorem Th4: :: PROCAL_1:4

for b₁, b₂ being Element of CQC-WFF holds b₁ => (b₂ 'or' b₁) in TAUT

proof end;

theorem Th5: :: PROCAL_1:5

for b₁, b₂ being Element of CQC-WFF holds (b₁ 'or' b₂) => (('not' b₁) => b₂) in TAUT

proof end;

theorem Th6: :: PROCAL_1:6

for b₁, b₂ being Element of CQC-WFF holds ('not' (b₁ 'or' b₂)) => (('not' b₁) '&' ('not' b₂)) in TAUT

proof end;

theorem Th7: :: PROCAL_1:7

for b₁, b₂ being Element of CQC-WFF holds (('not' b₁) '&' ('not' b₂)) => ('not' (b₁ 'or' b₂)) in TAUT

proof end;

theorem Th8: :: PROCAL_1:8

for b₁, b₂ being Element of CQC-WFF holds (b₁ 'or' b₂) => (b₂ 'or' b₁) in TAUT

proof end;

theorem Th9: :: PROCAL_1:9

for b₁ being Element of CQC-WFF holds ('not' b₁) 'or' b₁ in TAUT

proof end;

theorem Th10: :: PROCAL_1:10

for b₁, b₂ being Element of CQC-WFF holds ('not' (b₁ 'or' b₂)) => ('not' b₁) in TAUT

proof end;

theorem Th11: :: PROCAL_1:11

for b₁ being Element of CQC-WFF holds (b₁ 'or' b₁) => b₁ in TAUT

proof end;

theorem Th12: :: PROCAL_1:12

for b₁ being Element of CQC-WFF holds b₁ => (b₁ 'or' b₁) in TAUT by Th3;

theorem Th13: :: PROCAL_1:13

for b₁, b₂ being Element of CQC-WFF holds (b₁ '&' ('not' b₁)) => b₂ in TAUT

proof end;

theorem Th14: :: PROCAL_1:14

for b₁, b₂ being Element of CQC-WFF holds (b₁ => b₂) => (('not' b₁) 'or' b₂) in TAUT

proof end;

Lemma11: for b₁, b₂ being Element of CQC-WFF holds (b₁ '&' b₂) => (('not' ('not' b₁)) '&' b₂) in TAUT

proof end;

Lemma12: for b₁, b₂ being Element of CQC-WFF holds (('not' ('not' b₁)) '&' b₂) => (b₁ '&' b₂) in TAUT

proof end;

theorem Th15: :: PROCAL_1:15

for b₁, b₂ being Element of CQC-WFF holds (b₁ '&' b₂) => ('not' (b₁ => ('not' b₂))) in TAUT

proof end;

theorem Th16: :: PROCAL_1:16

for b₁, b₂ being Element of CQC-WFF holds ('not' (b₁ => ('not' b₂))) => (b₁ '&' b₂) in TAUT

proof end;

theorem Th17: :: PROCAL_1:17

for b₁, b₂ being Element of CQC-WFF holds ('not' (b₁ '&' b₂)) => (('not' b₁) 'or' ('not' b₂)) in TAUT

proof end;

theorem Th18: :: PROCAL_1:18

for b₁, b₂ being Element of CQC-WFF holds (('not' b₁) 'or' ('not' b₂)) => ('not' (b₁ '&' b₂)) in TAUT

proof end;

theorem Th19: :: PROCAL_1:19

for b₁, b₂ being Element of CQC-WFF holds (b₁ '&' b₂) => b₁ in TAUT

proof end;

theorem Th20: :: PROCAL_1:20

for b₁, b₂ being Element of CQC-WFF holds (b₁ '&' b₂) => (b₁ 'or' b₂) in TAUT

proof end;

theorem Th21: :: PROCAL_1:21

for b₁, b₂ being Element of CQC-WFF holds (b₁ '&' b₂) => b₂ in TAUT

proof end;

theorem Th22: :: PROCAL_1:22

for b₁ being Element of CQC-WFF holds b₁ => (b₁ '&' b₁) in TAUT

proof end;

theorem Th23: :: PROCAL_1:23

for b₁, b₂ being Element of CQC-WFF holds (b₁ <=> b₂) => (b₁ => b₂) in TAUT

proof end;

theorem Th24: :: PROCAL_1:24

for b₁, b₂ being Element of CQC-WFF holds (b₁ <=> b₂) => (b₂ => b₁) in TAUT

proof end;

theorem Th25: :: PROCAL_1:25

for b₁, b₂, b₃ being Element of CQC-WFF holds ((b₁ 'or' b₂) 'or' b₃) => (b₁ 'or' (b₂ 'or' b₃)) in TAUT

proof end;

theorem Th26: :: PROCAL_1:26

for b₁, b₂, b₃ being Element of CQC-WFF holds ((b₁ '&' b₂) '&' b₃) => (b₁ '&' (b₂ '&' b₃)) in TAUT

proof end;

theorem Th27: :: PROCAL_1:27

for b₁, b₂, b₃ being Element of CQC-WFF holds (b₁ 'or' (b₂ 'or' b₃)) => ((b₁ 'or' b₂) 'or' b₃) in TAUT

proof end;

theorem Th28: :: PROCAL_1:28

for b₁, b₂ being Element of CQC-WFF holds b₁ => (b₂ => (b₁ '&' b₂)) in TAUT

proof end;

theorem Th29: :: PROCAL_1:29

for b₁, b₂ being Element of CQC-WFF holds (b₁ => b₂) => ((b₂ => b₁) => (b₁ <=> b₂)) in TAUT

proof end;

Lemma23: for b₁, b₂ being Element of CQC-WFF st b₁ in TAUT & b₂ in TAUT holds
b₁ '&' b₂ in TAUT

proof end;

theorem Th30: :: PROCAL_1:30

for b₁, b₂ being Element of CQC-WFF holds (b₁ 'or' b₂) <=> (b₂ 'or' b₁) in TAUT

proof end;

theorem Th31: :: PROCAL_1:31

for b₁, b₂, b₃ being Element of CQC-WFF holds ((b₁ '&' b₂) => b₃) => (b₁ => (b₂ => b₃)) in TAUT

proof end;

theorem Th32: :: PROCAL_1:32

for b₁, b₂, b₃ being Element of CQC-WFF holds (b₁ => (b₂ => b₃)) => ((b₁ '&' b₂) => b₃) in TAUT

proof end;

theorem Th33: :: PROCAL_1:33

for b₁, b₂, b₃ being Element of CQC-WFF holds (b₁ => b₂) => ((b₁ => b₃) => (b₁ => (b₂ '&' b₃))) in TAUT

proof end;

theorem Th34: :: PROCAL_1:34

for b₁, b₂, b₃ being Element of CQC-WFF holds ((b₁ 'or' b₂) => b₃) => ((b₁ => b₃) 'or' (b₂ => b₃)) in TAUT

proof end;

theorem Th35: :: PROCAL_1:35

for b₁, b₂, b₃ being Element of CQC-WFF holds (b₁ => b₂) => ((b₃ => b₂) => ((b₁ 'or' b₃) => b₂)) in TAUT

proof end;

theorem Th36: :: PROCAL_1:36

for b₁, b₂, b₃ being Element of CQC-WFF holds ((b₁ => b₂) '&' (b₃ => b₂)) => ((b₁ 'or' b₃) => b₂) in TAUT

proof end;

theorem Th37: :: PROCAL_1:37

for b₁, b₂ being Element of CQC-WFF holds (b₁ => (b₂ '&' ('not' b₂))) => ('not' b₁) in TAUT

proof end;

theorem Th38: :: PROCAL_1:38

for b₁, b₂, b₃ being Element of CQC-WFF holds ((b₁ 'or' b₂) '&' (b₁ 'or' b₃)) => (b₁ 'or' (b₂ '&' b₃)) in TAUT

proof end;

theorem Th39: :: PROCAL_1:39

for b₁, b₂, b₃ being Element of CQC-WFF holds (b₁ '&' (b₂ 'or' b₃)) => ((b₁ '&' b₂) 'or' (b₁ '&' b₃)) in TAUT

proof end;

theorem Th40: :: PROCAL_1:40

for b₁, b₂, b₃ being Element of CQC-WFF holds ((b₁ 'or' b₂) '&' (b₃ 'or' b₂)) => ((b₁ '&' b₃) 'or' b₂) in TAUT

proof end;

Lemma29: for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => b₂ in TAUT holds
(b₃ '&' b₁) => (b₃ '&' b₂) in TAUT

proof end;

Lemma30: for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => b₂ in TAUT holds
(b₁ 'or' b₃) => (b₂ 'or' b₃) in TAUT

proof end;

Lemma31: for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => b₂ in TAUT holds
(b₃ 'or' b₁) => (b₃ 'or' b₂) in TAUT

proof end;

theorem Th41: :: PROCAL_1:41

for b₁, b₂, b₃ being Element of CQC-WFF holds ((b₁ 'or' b₂) '&' b₃) => ((b₁ '&' b₃) 'or' (b₂ '&' b₃)) in TAUT

proof end;

theorem Th42: :: PROCAL_1:42

for b₁, b₂ being Element of CQC-WFF st b₁ in TAUT holds
b₁ 'or' b₂ in TAUT

proof end;

theorem Th43: :: PROCAL_1:43

for b₁, b₂ being Element of CQC-WFF st b₁ in TAUT holds
b₂ 'or' b₁ in TAUT

proof end;

theorem Th44: :: PROCAL_1:44

for b₁, b₂ being Element of CQC-WFF st b₁ '&' b₂ in TAUT holds
b₁ in TAUT

proof end;

theorem Th45: :: PROCAL_1:45

for b₁, b₂ being Element of CQC-WFF st b₁ '&' b₂ in TAUT holds
b₂ in TAUT

proof end;

theorem Th46: :: PROCAL_1:46

for b₁, b₂ being Element of CQC-WFF st b₁ '&' b₂ in TAUT holds
b₁ 'or' b₂ in TAUT

proof end;

theorem Th47: :: PROCAL_1:47

for b₁, b₂ being Element of CQC-WFF st b₁ in TAUT & b₂ in TAUT holds
b₁ '&' b₂ in TAUT by Lemma23;

theorem Th48: :: PROCAL_1:48

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => b₂ in TAUT holds
(b₁ 'or' b₃) => (b₂ 'or' b₃) in TAUT by Lemma30;

theorem Th49: :: PROCAL_1:49

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => b₂ in TAUT holds
(b₃ 'or' b₁) => (b₃ 'or' b₂) in TAUT by Lemma31;

theorem Th50: :: PROCAL_1:50

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => b₂ in TAUT holds
(b₃ '&' b₁) => (b₃ '&' b₂) in TAUT by Lemma29;

theorem Th51: :: PROCAL_1:51

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => b₂ in TAUT holds
(b₁ '&' b₃) => (b₂ '&' b₃) in TAUT

proof end;

theorem Th52: :: PROCAL_1:52

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => b₂ in TAUT & b₁ => b₃ in TAUT holds
b₁ => (b₂ '&' b₃) in TAUT

proof end;

theorem Th53: :: PROCAL_1:53

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => b₂ in TAUT & b₃ => b₂ in TAUT holds
(b₁ 'or' b₃) => b₂ in TAUT

proof end;

theorem Th54: :: PROCAL_1:54

for b₁, b₂ being Element of CQC-WFF st b₁ 'or' b₂ in TAUT & 'not' b₁ in TAUT holds
b₂ in TAUT

proof end;

theorem Th55: :: PROCAL_1:55

for b₁, b₂ being Element of CQC-WFF st b₁ 'or' b₂ in TAUT & 'not' b₂ in TAUT holds
b₁ in TAUT

proof end;

theorem Th56: :: PROCAL_1:56

for b₁, b₂, b₃, b₄ being Element of CQC-WFF st b₁ => b₂ in TAUT & b₃ => b₄ in TAUT holds
(b₁ '&' b₃) => (b₂ '&' b₄) in TAUT

proof end;

theorem Th57: :: PROCAL_1:57

for b₁, b₂, b₃, b₄ being Element of CQC-WFF st b₁ => b₂ in TAUT & b₃ => b₄ in TAUT holds
(b₁ 'or' b₃) => (b₂ 'or' b₄) in TAUT

proof end;

theorem Th58: :: PROCAL_1:58

for b₁, b₂ being Element of CQC-WFF st (b₁ '&' ('not' b₂)) => ('not' b₁) in TAUT holds
b₁ => b₂ in TAUT

proof end;