theorem :: HILBERT1:50

for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' q) '&' s) in HP_TAUT