begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
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:
theorem Th6:
theorem Th7:
theorem
canceled;
theorem Th9:
theorem Th10:
theorem
theorem
theorem
canceled;
theorem Th14:
theorem
theorem
canceled;
theorem
theorem Th18:
theorem Th19:
theorem
theorem
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem
theorem
theorem
theorem
canceled;
theorem Th34:
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem
theorem Th43:
theorem Th44:
theorem Th45:
theorem
theorem Th47:
theorem
theorem Th49:
theorem
theorem Th51:
theorem
theorem Th53:
theorem
theorem Th55:
theorem
theorem
theorem Th58:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th65:
theorem Th66:
theorem
theorem Th68:
theorem Th69:
theorem Th70:
theorem
theorem Th72:
theorem Th73:
theorem
theorem Th75:
theorem Th76:
theorem
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:
theorem Th79:
theorem
theorem Th81:
theorem Th82:
theorem
theorem Th84:
theorem Th85:
theorem
theorem Th87:
theorem Th88:
theorem Th89:
theorem
theorem
theorem Th92:
theorem
theorem Th94:
theorem
theorem