theorem Th54: :: CQC_THE3:54

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