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