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