let A be QC-alphabet ; :: thesis: for p, q, r being Element of CQC-WFF A st p |- q & q |- r holds
p |- r
let p, q, r be Element of CQC-WFF A; :: thesis: ( p |- q & q |- r implies p |- r )
assume that
A1: p |- q and
A2: q |- r ; :: thesis: p |- r
A3: {q} |- r by A2, Def1;
{p} |- q by A1, Def1;
then {p} |- r by A3, Th3;
hence p |- r by Def1; :: thesis: verum