let A be QC-alphabet ; :: thesis: for p, q, r being Element of CQC-WFF A st p => q is valid & q => r is valid holds
p => r is valid
let p, q, r be Element of CQC-WFF A; :: 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 A & q => r in TAUT A ) by CQC_THE1:def 10;
hence p => r in TAUT A by Th3; :: according to CQC_THE1:def 10 :: thesis: verum