:: Calculus of Propositions :: by Jan Popio{\l}ek and Andrzej Trybulec :: :: Received October 23, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin 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 proofend; Lm1: for A being QC-alphabet for p, q being Element of CQC-WFF A holds p 'or' q = ('not' p) => q proofend; 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 proofend; 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 proofend; theorem Th4: :: PROCAL_1:4 for A being QC-alphabet for q, p being Element of CQC-WFF A holds q => (p 'or' q) in TAUT A proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem :: PROCAL_1:22 for A being QC-alphabet for p being Element of CQC-WFF A holds p => (p '&' p) in TAUT A proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th33: :: PROCAL_1:33 for A being QC-alphabet for r, p, q being Element of CQC-WFF A holds (r => p) => ((r => q) => (r => (p '&' q))) in TAUT A proofend; 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 proofend; theorem Th35: :: PROCAL_1:35 for A being QC-alphabet for p, r, q being Element of CQC-WFF A holds (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A proofend; theorem Th36: :: PROCAL_1:36 for A being QC-alphabet for p, r, q being Element of CQC-WFF A holds ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT A proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th40: :: PROCAL_1:40 for A being QC-alphabet for p, r, q being Element of CQC-WFF A holds ((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r) in TAUT A proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; :: 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 proofend; theorem :: PROCAL_1:43 for A being QC-alphabet for q, p being Element of CQC-WFF A st q in TAUT A holds p 'or' q in TAUT A proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem :: PROCAL_1:52 for A being QC-alphabet for r, p, q being Element of CQC-WFF A st r => p in TAUT A & r => q in TAUT A holds r => (p '&' q) in TAUT A proofend; theorem :: PROCAL_1:53 for A being QC-alphabet for p, r, q 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend;