theorem Th27: :: PROCAL_1:27

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (p 'or' (q 'or' r)) => ((p 'or' q) 'or' r) in TAUT A