begin
Lm1:
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( (p '&' q) => p is valid & (p '&' q) => q is valid )
Lm2:
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p '&' q is valid holds
( p is valid & q is valid )
Lm3:
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid & p => r is valid holds
p => (q '&' r) is valid
Lm4:
for A being QC-alphabet
for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds
(p 'or' r) => (q 'or' t) is valid
Lm5:
for A being QC-alphabet
for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds
(p '&' r) => (q '&' t) is valid
Lm6:
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p => (p 'or' q) is valid & p => (q 'or' p) is valid )
Lm7:
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid & r => q is valid holds
(p 'or' r) => q is valid
Lm8:
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is valid & q is valid holds
p '&' q is valid
Lm9:
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid holds
(r '&' p) => (r '&' q) is valid
Lm10:
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid holds
(p 'or' r) => (q 'or' r) is valid
Lm11:
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p 'or' q) => (('not' p) => q) is valid
Lm12:
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (('not' p) => q) => (p 'or' q) is valid
Lm13:
for A being QC-alphabet
for p being Element of CQC-WFF A holds p <=> p is valid
Lm14:
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( ( p => q is valid & q => p is valid ) iff p <=> q is valid )
Lm15:
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p <=> q is valid holds
( p is valid iff q is valid )
Lm16:
for A being QC-alphabet
for p, q, r, t being Element of CQC-WFF A st p => (q => r) is valid & r => t is valid holds
p => (q => t) is valid
Lm17:
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(All (x,(p => q))) => (p => (All (x,q))) is valid