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