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 is valid by A1, Th50;
A4: q => p is valid by A1, Th50;
A5: q => r is valid by A2, Th50;
A6: r => q is valid by A2, Th50;
A7: p => r is valid by A3, A5, LUKASI_1:43;
r => p is valid by A4, A6, LUKASI_1:43;
hence p <==> r by A7, Th50; :: thesis: verum