let p, q, r be Element of CQC-WFF ; :: thesis: ( p |-| q & q |-| r implies p |-| r )
assume that
A1: p |-| q and
A2: q |-| r ; :: thesis: p |-| r
A3: p |- q by A1, Def5;
q |- r by A2, Def5;
then A4: p |- r by A3, Th6;
A5: q |- p by A1, Def5;
r |- q by A2, Def5;
then r |- p by A5, Th6;
hence p |-| r by A4, Def5; :: thesis: verum