begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
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:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
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:
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:
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem
theorem
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem
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:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem
theorem
theorem Th34:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem Th43:
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem Th48:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem Th55:
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem Th76:
theorem
theorem
theorem
theorem Th80:
theorem
theorem
theorem
theorem Th84:
theorem
theorem
theorem
theorem
theorem
theorem Th90:
theorem Th91:
theorem
theorem