let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds ('not' p) => (p => q) in TAUT A
let p, q be Element of CQC-WFF A; :: thesis: ('not' p) => (p => q) in TAUT A
( ('not' p) => (('not' ('not' p)) => q) in TAUT A & (('not' ('not' p)) => q) => (p => q) in TAUT A ) by Th28, CQC_THE1:43;
hence ('not' p) => (p => q) in TAUT A by Th3; :: thesis: verum