let p, q, r be Element of CQC-WFF ; :: thesis: ((('not' p) => q) => r) => (p => r) in TAUT
p => (('not' p) => q) in TAUT by CQC_THE1:43;
hence ((('not' p) => q) => r) => (p => r) in TAUT by Th2; :: thesis: verum