let A be QC-alphabet ; :: thesis: for p, q, r, t being Element of CQC-WFF A st p => (q => r) is valid & r => t is valid holds
p => (q => t) is valid
let p, q, r, t be Element of CQC-WFF A; :: 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