:: Propositional Calculus
:: by Grzegorz Bancerek, Agata Darmochwa\l and Andrzej Trybulec
::
:: Received September 26, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: LUKASI_1:1
theorem Th2: :: LUKASI_1:2
theorem Th3: :: LUKASI_1:3
theorem Th4: :: LUKASI_1:4
Lm1:
for q, r, p, s being Element of CQC-WFF holds (((q => r) => (p => r)) => s) => ((p => q) => s) in TAUT
Lm2:
for p, q, r, s being Element of CQC-WFF holds (p => (q => r)) => ((s => q) => (p => (s => r))) in TAUT
Lm3:
for p, q, r, s being Element of CQC-WFF holds (p => q) => (((p => r) => s) => ((q => r) => s)) in TAUT
Lm4:
for t, p, r, s, q being Element of CQC-WFF holds (t => ((p => r) => s)) => ((p => q) => (t => ((q => r) => s))) in TAUT
Lm5:
for p, q, r being Element of CQC-WFF holds ((('not' p) => q) => r) => (p => r) in TAUT
Lm6:
for p, r, s, q being Element of CQC-WFF holds p => (((('not' p) => r) => s) => ((q => r) => s)) in TAUT
Lm7:
for q, p being Element of CQC-WFF holds (q => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT
Lm8:
for t, p being Element of CQC-WFF holds t => ((('not' p) => p) => p) in TAUT
Lm9:
for p, q, t being Element of CQC-WFF holds (('not' p) => q) => (t => ((q => p) => p)) in TAUT
Lm10:
for t, q, p, r being Element of CQC-WFF holds ((t => ((q => p) => p)) => r) => ((('not' p) => q) => r) in TAUT
Lm11:
for p, q being Element of CQC-WFF holds (('not' p) => q) => ((q => p) => p) in TAUT
Lm12:
for p, q being Element of CQC-WFF holds p => ((q => p) => p) in TAUT
theorem Th5: :: LUKASI_1:5
theorem Th6: :: LUKASI_1:6
theorem Th7: :: LUKASI_1:7
theorem Th8: :: LUKASI_1:8
theorem Th9: :: LUKASI_1:9
Lm13:
for q, s, p, r being Element of CQC-WFF holds ((q => (s => p)) => r) => ((s => (q => p)) => r) in TAUT
Lm14:
for p, q being Element of CQC-WFF holds ((p => q) => p) => p in TAUT
Lm15:
for p, r, s, q being Element of CQC-WFF holds ((p => r) => s) => ((p => q) => ((q => r) => s)) in TAUT
Lm16:
for p, q, r being Element of CQC-WFF holds ((p => q) => r) => ((r => p) => p) in TAUT
Lm17:
for r, p, s, q being Element of CQC-WFF holds (((r => p) => p) => s) => (((p => q) => r) => s) in TAUT
Lm18:
for q, r, p being Element of CQC-WFF holds ((q => r) => p) => ((q => p) => p) in TAUT
theorem Th10: :: LUKASI_1:10
Lm19:
for q, s, r, p being Element of CQC-WFF holds (q => s) => (((q => r) => p) => ((s => p) => p)) in TAUT
Lm20:
for q, r, p, s being Element of CQC-WFF holds ((q => r) => p) => ((q => s) => ((s => p) => p)) in TAUT
Lm21:
for q, s, p, r being Element of CQC-WFF holds (q => s) => ((s => (p => (q => r))) => (p => (q => r))) in TAUT
Lm22:
for s, p, q, r being Element of CQC-WFF holds (s => (p => (q => r))) => ((q => s) => (p => (q => r))) in TAUT
theorem Th11: :: LUKASI_1:11
theorem Th12: :: LUKASI_1:12
theorem Th13: :: LUKASI_1:13
theorem :: LUKASI_1:14
theorem Th15: :: LUKASI_1:15
theorem Th16: :: LUKASI_1:16
theorem :: LUKASI_1:17
theorem :: LUKASI_1:18
theorem Th19: :: LUKASI_1:19
theorem Th20: :: LUKASI_1:20
theorem :: LUKASI_1:21
theorem Th22: :: LUKASI_1:22
theorem :: LUKASI_1:23
Lm23:
for p being Element of CQC-WFF holds ('not' p) => (p => ('not' VERUM )) in TAUT
Lm24:
for p being Element of CQC-WFF holds (('not' p) => ('not' VERUM )) => p in TAUT
theorem Th24: :: LUKASI_1:24
theorem Th25: :: LUKASI_1:25
theorem Th26: :: LUKASI_1:26
theorem Th27: :: LUKASI_1:27
theorem Th28: :: LUKASI_1:28
theorem Th29: :: LUKASI_1:29
theorem Th30: :: LUKASI_1:30
theorem Th31: :: LUKASI_1:31
theorem :: LUKASI_1:32
theorem :: LUKASI_1:33
theorem Th34: :: LUKASI_1:34
theorem :: LUKASI_1:35
theorem :: LUKASI_1:36
theorem :: LUKASI_1:37
theorem :: LUKASI_1:38
theorem :: LUKASI_1:39
theorem :: LUKASI_1:40
theorem Th41: :: LUKASI_1:41
theorem :: LUKASI_1:42
theorem Th43: :: LUKASI_1:43
theorem Th44: :: LUKASI_1:44
theorem Th45: :: LUKASI_1:45
theorem :: LUKASI_1:46
theorem Th47: :: LUKASI_1:47
theorem Th48: :: LUKASI_1:48
theorem :: LUKASI_1:49
theorem :: LUKASI_1:50
theorem Th51: :: LUKASI_1:51
theorem Th52: :: LUKASI_1:52
theorem :: LUKASI_1:53
theorem Th54: :: LUKASI_1:54
theorem Th55: :: LUKASI_1:55
theorem :: LUKASI_1:56
theorem Th57: :: LUKASI_1:57
theorem :: LUKASI_1:58
theorem Th59: :: LUKASI_1:59
theorem :: LUKASI_1:60
theorem Th61: :: LUKASI_1:61
theorem Th62: :: LUKASI_1:62
theorem :: LUKASI_1:63
theorem Th64: :: LUKASI_1:64
theorem Th65: :: LUKASI_1:65
theorem :: LUKASI_1:66
theorem Th67: :: LUKASI_1:67
theorem :: LUKASI_1:68
theorem Th69: :: LUKASI_1:69
theorem :: LUKASI_1:70
theorem Th71: :: LUKASI_1:71
theorem :: LUKASI_1:72
theorem Th73: :: LUKASI_1:73
theorem :: LUKASI_1:74
theorem :: LUKASI_1:75
theorem Th76: :: LUKASI_1:76
theorem :: LUKASI_1:77
theorem :: LUKASI_1:78
theorem :: LUKASI_1:79
theorem Th80: :: LUKASI_1:80
theorem :: LUKASI_1:81
theorem :: LUKASI_1:82
theorem :: LUKASI_1:83
theorem Th84: :: LUKASI_1:84
theorem :: LUKASI_1:85
theorem :: LUKASI_1:86
theorem :: LUKASI_1:87
theorem :: LUKASI_1:88
theorem :: LUKASI_1:89
theorem Th90: :: LUKASI_1:90
theorem Th91: :: LUKASI_1:91
theorem :: LUKASI_1:92
theorem :: LUKASI_1:93