theorem :: HILBERT1:47

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