theorem :: CQC_THE3:57

for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds
p <=> r <==> q <=> s