:: Calculus of Quantifiers. Deduction Theorem
:: by Agata Darmochwa\l
::
:: Received October 24, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: CQC_THE2:1
theorem Th2: :: CQC_THE2:2
theorem Th3: :: CQC_THE2:3
theorem Th4: :: CQC_THE2:4
Lm1:
for p, q being Element of CQC-WFF holds
( (p '&' q) => p is valid & (p '&' q) => q is valid )
Lm2:
for p, q being Element of CQC-WFF st p '&' q is valid holds
( p is valid & q is valid )
Lm3:
for p, q, r being Element of CQC-WFF st p => q is valid & p => r is valid holds
p => (q '&' r) is valid
Lm4:
for p, q, r, t being Element of CQC-WFF st p => q is valid & r => t is valid holds
(p 'or' r) => (q 'or' t) is valid
Lm5:
for p, q, r, t being Element of CQC-WFF st p => q is valid & r => t is valid holds
(p '&' r) => (q '&' t) is valid
Lm6:
for p, q being Element of CQC-WFF holds
( p => (p 'or' q) is valid & p => (q 'or' p) is valid )
Lm7:
for p, q, r being Element of CQC-WFF st p => q is valid & r => q is valid holds
(p 'or' r) => q is valid
Lm8:
for p, q being Element of CQC-WFF st p is valid & q is valid holds
p '&' q is valid
Lm9:
for p, q, r being Element of CQC-WFF st p => q is valid holds
(r '&' p) => (r '&' q) is valid
Lm10:
for p, q, r being Element of CQC-WFF st p => q is valid holds
(p 'or' r) => (q 'or' r) is valid
Lm11:
for p, q being Element of CQC-WFF holds (p 'or' q) => (('not' p) => q) is valid
Lm12:
for p, q being Element of CQC-WFF holds (('not' p) => q) => (p 'or' q) is valid
Lm13:
for p being Element of CQC-WFF holds p <=> p is valid
Lm14:
for p, q being Element of CQC-WFF holds
( ( p => q is valid & q => p is valid ) iff p <=> q is valid )
Lm15:
for p, q being Element of CQC-WFF st p <=> q is valid holds
( p is valid iff q is valid )
Lm16:
for p, q, r, t being Element of CQC-WFF st p => (q => r) is valid & r => t is valid holds
p => (q => t) is valid
theorem Th5: :: CQC_THE2:5
theorem Th6: :: CQC_THE2:6
theorem Th7: :: CQC_THE2:7
theorem :: CQC_THE2:8
canceled;
theorem Th9: :: CQC_THE2:9
theorem Th10: :: CQC_THE2:10
theorem :: CQC_THE2:11
theorem :: CQC_THE2:12
theorem :: CQC_THE2:13
canceled;
theorem Th14: :: CQC_THE2:14
theorem :: CQC_THE2:15
theorem :: CQC_THE2:16
canceled;
theorem :: CQC_THE2:17
theorem Th18: :: CQC_THE2:18
theorem Th19: :: CQC_THE2:19
theorem :: CQC_THE2:20
theorem :: CQC_THE2:21
theorem Th22: :: CQC_THE2:22
theorem Th23: :: CQC_THE2:23
theorem :: CQC_THE2:24
theorem Th25: :: CQC_THE2:25
theorem Th26: :: CQC_THE2:26
theorem Th27: :: CQC_THE2:27
theorem Th28: :: CQC_THE2:28
theorem :: CQC_THE2:29
theorem :: CQC_THE2:30
theorem :: CQC_THE2:31
theorem :: CQC_THE2:32
theorem :: CQC_THE2:33
canceled;
theorem Th34: :: CQC_THE2:34
theorem Th35: :: CQC_THE2:35
theorem Th36: :: CQC_THE2:36
theorem :: CQC_THE2:37
theorem Th38: :: CQC_THE2:38
theorem Th39: :: CQC_THE2:39
theorem Th40: :: CQC_THE2:40
theorem Th41: :: CQC_THE2:41
theorem :: CQC_THE2:42
theorem Th43: :: CQC_THE2:43
theorem Th44: :: CQC_THE2:44
theorem Th45: :: CQC_THE2:45
theorem :: CQC_THE2:46
theorem Th47: :: CQC_THE2:47
theorem :: CQC_THE2:48
theorem Th49: :: CQC_THE2:49
theorem :: CQC_THE2:50
theorem Th51: :: CQC_THE2:51
theorem :: CQC_THE2:52
theorem Th53: :: CQC_THE2:53
theorem :: CQC_THE2:54
theorem Th55: :: CQC_THE2:55
theorem :: CQC_THE2:56
theorem :: CQC_THE2:57
theorem Th58: :: CQC_THE2:58
theorem :: CQC_THE2:59
theorem :: CQC_THE2:60
theorem :: CQC_THE2:61
theorem :: CQC_THE2:62
theorem :: CQC_THE2:63
theorem :: CQC_THE2:64
theorem Th65: :: CQC_THE2:65
theorem Th66: :: CQC_THE2:66
theorem :: CQC_THE2:67
theorem Th68: :: CQC_THE2:68
theorem Th69: :: CQC_THE2:69
theorem Th70: :: CQC_THE2:70
theorem :: CQC_THE2:71
theorem Th72: :: CQC_THE2:72
theorem Th73: :: CQC_THE2:73
theorem :: CQC_THE2:74
theorem Th75: :: CQC_THE2:75
theorem Th76: :: CQC_THE2:76
theorem :: CQC_THE2:77
Lm17:
for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
(All x,(p => q)) => (p => (All x,q)) is valid
theorem Th78: :: CQC_THE2:78
theorem Th79: :: CQC_THE2:79
theorem :: CQC_THE2:80
theorem Th81: :: CQC_THE2:81
theorem Th82: :: CQC_THE2:82
theorem :: CQC_THE2:83
theorem Th84: :: CQC_THE2:84
theorem Th85: :: CQC_THE2:85
theorem :: CQC_THE2:86
theorem Th87: :: CQC_THE2:87
theorem Th88: :: CQC_THE2:88
theorem Th89: :: CQC_THE2:89
theorem :: CQC_THE2:90
theorem :: CQC_THE2:91
theorem Th92: :: CQC_THE2:92
theorem :: CQC_THE2:93
theorem Th94: :: CQC_THE2:94
theorem Th95: :: CQC_THE2:95
theorem :: CQC_THE2:96