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

begin

theorem Th1: :: PROCAL_1:1

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

proof end;

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

proof end;

theorem Th2: :: PROCAL_1:2

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

proof end;

theorem Th3: :: PROCAL_1:3

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

proof end;

theorem Th4: :: PROCAL_1:4

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

proof end;

theorem Th5: :: PROCAL_1:5

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

proof end;

theorem Th6: :: PROCAL_1:6

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

proof end;

theorem Th7: :: PROCAL_1:7

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

proof end;

theorem Th8: :: PROCAL_1:8

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

proof end;

theorem :: PROCAL_1:9

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

proof end;

theorem :: PROCAL_1:10

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

proof end;

theorem Th11: :: PROCAL_1:11

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

proof end;

theorem :: PROCAL_1:12

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

theorem :: PROCAL_1:13

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

proof end;

theorem :: PROCAL_1:14

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

proof end;

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

proof end;

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

proof end;

theorem Th15: :: PROCAL_1:15

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

proof end;

theorem Th16: :: PROCAL_1:16

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

proof end;

theorem Th17: :: PROCAL_1:17

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

proof end;

theorem Th18: :: PROCAL_1:18

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

proof end;

theorem Th19: :: PROCAL_1:19

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

proof end;

theorem Th20: :: PROCAL_1:20

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

proof end;

theorem Th21: :: PROCAL_1:21

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

proof end;

theorem :: PROCAL_1:22

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

proof end;

theorem :: PROCAL_1:23

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

proof end;

theorem :: PROCAL_1:24

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

proof end;

theorem Th25: :: PROCAL_1:25

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

proof end;

theorem :: PROCAL_1:26

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

proof end;

theorem Th27: :: PROCAL_1:27

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

proof end;

theorem Th28: :: PROCAL_1:28

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

proof end;

theorem :: PROCAL_1:29

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

proof end;

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

proof end;

theorem :: PROCAL_1:30

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

proof end;

theorem :: PROCAL_1:31

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

proof end;

theorem Th32: :: PROCAL_1:32

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

proof end;

theorem Th33: :: PROCAL_1:33

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

proof end;

theorem :: PROCAL_1:34

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

proof end;

theorem Th35: :: PROCAL_1:35

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

proof end;

theorem Th36: :: PROCAL_1:36

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

proof end;

theorem :: PROCAL_1:37

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

proof end;

theorem :: PROCAL_1:38

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

proof end;

theorem :: PROCAL_1:39

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

proof end;

theorem Th40: :: PROCAL_1:40

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem :: PROCAL_1:41

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

proof end;

theorem :: PROCAL_1:42

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

proof end;

theorem :: PROCAL_1:43

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

proof end;

theorem :: PROCAL_1:44

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

proof end;

theorem :: PROCAL_1:45

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

proof end;

theorem :: PROCAL_1:46

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

proof end;

theorem :: PROCAL_1:47

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

theorem :: PROCAL_1:48

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

theorem :: PROCAL_1:49

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

theorem :: PROCAL_1:50

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

theorem Th51: :: PROCAL_1:51

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

proof end;

theorem :: PROCAL_1:52

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

proof end;

theorem :: PROCAL_1:53

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

proof end;

theorem :: PROCAL_1:54

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

proof end;

theorem :: PROCAL_1:55

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

proof end;

theorem :: PROCAL_1:56

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

proof end;

theorem :: PROCAL_1:57

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

proof end;

theorem :: PROCAL_1:58

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

proof end;