:: by Jan Popio{\l}ek and Andrzej Trybulec

::

:: Received October 23, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

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 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

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

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

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

for p, q being Element of CQC-WFF A holds (p 'or' q) => (q '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

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

proof end;

theorem :: PROCAL_1:12

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

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

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

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

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

for p, q being Element of CQC-WFF A holds (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) 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

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

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

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: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

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

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

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

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

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

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

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

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

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

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

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

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

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: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

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

theorem :: PROCAL_1:48

theorem :: PROCAL_1:49

theorem :: PROCAL_1:50

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

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

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

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

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

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

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

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

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;