:: Calculus of Propositions
:: by Jan Popio{\l}ek and Andrzej Trybulec
::
:: Received October 23, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

theorem Th1: :: PROCAL_1:1

for A being QC-alphabet
for p being Element of CQC-WFF A holds 'not' (p '&' ('not' p)) in TAUT A

proof end;

Lm1: for A being QC-alphabet
for p, q being Element of CQC-WFF A holds p 'or' q = ('not' p) => q

proof end;

theorem Th2: :: PROCAL_1:2

for A being QC-alphabet
for p being Element of CQC-WFF A holds p 'or' ('not' p) in TAUT A

proof end;

theorem Th3: :: PROCAL_1:3

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds p => (p 'or' q) in TAUT A

proof end;

theorem Th4: :: PROCAL_1:4

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds q => (p 'or' q) in TAUT A

proof end;

theorem Th5: :: PROCAL_1:5

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p 'or' q) => (('not' p) => q) in TAUT A

proof end;

theorem Th6: :: PROCAL_1:6

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) in TAUT A

proof end;

theorem Th7: :: PROCAL_1:7

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) in TAUT A

proof end;

theorem Th8: :: PROCAL_1:8

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p 'or' q) => (q 'or' p) in TAUT A

proof end;

theorem :: PROCAL_1:9

for A being QC-alphabet
for p being Element of CQC-WFF A holds ('not' p) 'or' p in TAUT A

proof end;

theorem :: PROCAL_1:10

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds ('not' (p 'or' q)) => ('not' p) in TAUT A

proof end;

theorem Th11: :: PROCAL_1:11

for A being QC-alphabet
for p being Element of CQC-WFF A holds (p 'or' p) => p in TAUT A

proof end;

theorem :: PROCAL_1:12

for A being QC-alphabet
for p being Element of CQC-WFF A holds p => (p 'or' p) in TAUT A by Th3;

theorem :: PROCAL_1:13

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p '&' ('not' p)) => q in TAUT A

proof end;

theorem :: PROCAL_1:14

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p => q) => (('not' p) 'or' q) in TAUT A

proof end;

Lm2: for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p '&' q) => (('not' ('not' p)) '&' q) in TAUT A

proof end;

Lm3: for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (('not' ('not' p)) '&' q) => (p '&' q) in TAUT A

proof end;

theorem Th15: :: PROCAL_1:15

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p '&' q) => ('not' (p => ('not' q))) in TAUT A

proof end;

theorem Th16: :: PROCAL_1:16

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds ('not' (p => ('not' q))) => (p '&' q) in TAUT A

proof end;

theorem Th17: :: PROCAL_1:17

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT A

proof end;

theorem Th18: :: PROCAL_1:18

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) in TAUT A

proof end;

theorem Th19: :: PROCAL_1:19

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p '&' q) => p in TAUT A

proof end;

theorem Th20: :: PROCAL_1:20

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p '&' q) => (p 'or' q) in TAUT A

proof end;

theorem Th21: :: PROCAL_1:21

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p '&' q) => q in TAUT A

proof end;

theorem :: PROCAL_1:22

for A being QC-alphabet
for p being Element of CQC-WFF A holds p => (p '&' p) in TAUT A

proof end;

theorem :: PROCAL_1:23

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p <=> q) => (p => q) in TAUT A

proof end;

theorem :: PROCAL_1:24

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p <=> q) => (q => p) in TAUT A

proof end;

theorem Th25: :: PROCAL_1:25

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p 'or' q) 'or' r) => (p 'or' (q 'or' r)) in TAUT A

proof end;

theorem :: PROCAL_1:26

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p '&' q) '&' r) => (p '&' (q '&' r)) in TAUT A

proof end;

theorem Th27: :: PROCAL_1:27

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (p 'or' (q 'or' r)) => ((p 'or' q) 'or' r) in TAUT A

proof end;

theorem Th28: :: PROCAL_1:28

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds p => (q => (p '&' q)) in TAUT A

proof end;

theorem :: PROCAL_1:29

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p => q) => ((q => p) => (p <=> q)) in TAUT A

proof end;

Lm4: for A being QC-alphabet
for p, q being Element of CQC-WFF A st p in TAUT A & q in TAUT A holds
p '&' q in TAUT A

proof end;

theorem :: PROCAL_1:30

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p 'or' q) <=> (q 'or' p) in TAUT A

proof end;

theorem :: PROCAL_1:31

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p '&' q) => r) => (p => (q => r)) in TAUT A

proof end;

theorem Th32: :: PROCAL_1:32

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (p => (q => r)) => ((p '&' q) => r) in TAUT A

proof end;

theorem Th33: :: PROCAL_1:33

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (r => p) => ((r => q) => (r => (p '&' q))) in TAUT A

proof end;

theorem :: PROCAL_1:34

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p 'or' q) => r) => ((p => r) 'or' (q => r)) in TAUT A

proof end;

theorem Th35: :: PROCAL_1:35

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A

proof end;

theorem Th36: :: PROCAL_1:36

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT A

proof end;

theorem :: PROCAL_1:37

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p => (q '&' ('not' q))) => ('not' p) in TAUT A

proof end;

theorem :: PROCAL_1:38

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT A

proof end;

theorem :: PROCAL_1:39

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT A

proof end;

theorem Th40: :: PROCAL_1:40

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r) in TAUT A

proof end;

Lm5: for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(r '&' p) => (r '&' q) in TAUT A

proof end;

Lm6: for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(p 'or' r) => (q 'or' r) in TAUT A

proof end;

Lm7: for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(r 'or' p) => (r 'or' q) in TAUT A

proof end;

theorem :: PROCAL_1:41

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT A

proof end;

:: Deduction Rules

theorem :: PROCAL_1:42

for A being QC-alphabet
for p, q being Element of CQC-WFF A st p in TAUT A holds
p 'or' q in TAUT A

proof end;

theorem :: PROCAL_1:43

for A being QC-alphabet
for p, q being Element of CQC-WFF A st q in TAUT A holds
p 'or' q in TAUT A

proof end;

theorem :: PROCAL_1:44

for A being QC-alphabet
for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds
p in TAUT A

proof end;

theorem :: PROCAL_1:45

for A being QC-alphabet
for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds
q in TAUT A

proof end;

theorem :: PROCAL_1:46

for A being QC-alphabet
for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds
p 'or' q in TAUT A

proof end;

theorem :: PROCAL_1:47

for A being QC-alphabet
for p, q being Element of CQC-WFF A st p in TAUT A & q in TAUT A holds
p '&' q in TAUT A by Lm4;

theorem :: PROCAL_1:48

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(p 'or' r) => (q 'or' r) in TAUT A by Lm6;

theorem :: PROCAL_1:49

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(r 'or' p) => (r 'or' q) in TAUT A by Lm7;

theorem :: PROCAL_1:50

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(r '&' p) => (r '&' q) in TAUT A by Lm5;

theorem Th51: :: PROCAL_1:51

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(p '&' r) => (q '&' r) in TAUT A

proof end;

theorem :: PROCAL_1:52

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st r => p in TAUT A & r => q in TAUT A holds
r => (p '&' q) in TAUT A

proof end;

theorem :: PROCAL_1:53

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => r in TAUT A & q => r in TAUT A holds
(p 'or' q) => r in TAUT A

proof end;

theorem :: PROCAL_1:54

for A being QC-alphabet
for p, q being Element of CQC-WFF A st p 'or' q in TAUT A & 'not' p in TAUT A holds
q in TAUT A

proof end;

theorem :: PROCAL_1:55

for A being QC-alphabet
for p, q being Element of CQC-WFF A st p 'or' q in TAUT A & 'not' q in TAUT A holds
p in TAUT A

proof end;

theorem :: PROCAL_1:56

for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p => q in TAUT A & r => s in TAUT A holds
(p '&' r) => (q '&' s) in TAUT A

proof end;

theorem :: PROCAL_1:57

for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p => q in TAUT A & r => s in TAUT A holds
(p 'or' r) => (q 'or' s) in TAUT A

proof end;

theorem :: PROCAL_1:58

for A being QC-alphabet
for p, q being Element of CQC-WFF A st (p '&' ('not' q)) => ('not' p) in TAUT A holds
p => q in TAUT A

proof end;