theorem :: CQC_THE3:56

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