let A be QC-alphabet ; :: thesis: for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds
p <=> r <==> q <=> s
let p, q, r, s be Element of CQC-WFF A; :: thesis: ( p <==> q & r <==> s implies p <=> r <==> q <=> s )
assume that
A1: p <==> q and
A2: r <==> s ; :: thesis: p <=> r <==> q <=> s
A3: r => p <==> s => q by A1, A2, Th55;
A4: p <=> r = (p => r) '&' (r => p) by QC_LANG2:def 4;
p => r <==> q => s by A1, A2, Th55;
then (p => r) '&' (r => p) <==> (q => s) '&' (s => q) by A3, Th54;
hence p <=> r <==> q <=> s by A4, QC_LANG2:def 4; :: thesis: verum