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 that
A1: p => (q => r) is valid and
A2: r => t is valid ; :: thesis: p => (q => t) is valid
(p '&' q) => r is valid by A1, Th1;
then (p '&' q) => t is valid by A2, LUKASI_1:42;
hence p => (q => t) is valid by Th3; :: thesis: verum