let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds (p => q) => (('not' q) => ('not' p)) in TAUT A
let p, q be Element of CQC-WFF A; :: thesis: (p => q) => (('not' q) => ('not' p)) in TAUT A
( ('not' q) => (q => ('not' (VERUM A))) in TAUT A & (q => ('not' (VERUM A))) => ((p => q) => (p => ('not' (VERUM A)))) in TAUT A ) by Lm23, Th9;
then A1: ('not' q) => ((p => q) => (p => ('not' (VERUM A)))) in TAUT A by Th3;
('not' q) => ((p => ('not' (VERUM A))) => ('not' p)) in TAUT A by Lm25, Th13;
then ('not' q) => ((p => q) => ('not' p)) in TAUT A by A1, Th22;
hence (p => q) => (('not' q) => ('not' p)) in TAUT A by Th15; :: thesis: verum