let p, q, r, t be Element of CQC-WFF ; :: thesis: ( p => (q => r) is valid & r => t is valid implies p => (q => t) is valid )
assume ( p => (q => r) is valid & r => t is valid ) ; :: thesis: p => (q => t) is valid
then ( (p '&' q) => r is valid & r => t is valid ) by Th1;
then (p '&' q) => t is valid by LUKASI_1:43;
hence p => (q => t) is valid by Th3; :: thesis: verum