let p, q, r be Element of CQC-WFF ; :: thesis: ( p => q in TAUT & q => r in TAUT implies p => r in TAUT )
assume that
A1: p => q in TAUT and
A2: q => r in TAUT ; :: thesis: p => r in TAUT
(p => q) => ((q => r) => (p => r)) in TAUT by Th1;
then (q => r) => (p => r) in TAUT by A1, CQC_THE1:46;
hence p => r in TAUT by A2, CQC_THE1:46; :: thesis: verum