theorem Th25: :: PROCAL_1:25

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