let p, q, r be Element of CQC-WFF ; :: thesis: ( (p => q) => r is valid implies q => r is valid )
assume A1: (p => q) => r is valid ; :: thesis: q => r is valid
((p => q) => r) => (q => r) is valid by Th57;
hence q => r is valid by A1, CQC_THE1:104; :: thesis: verum