let p, q, r be Element of CQC-WFF ; :: thesis: ( p => q is valid & q => r is valid implies p => r is valid )
assume ( p => q is valid & q => r is valid ) ; :: thesis: p => r is valid
then ( p => q in TAUT & q => r in TAUT ) by CQC_THE1:def 10;
hence p => r in TAUT by Th3; :: according to CQC_THE1:def 10 :: thesis: verum