theorem :: HILBERT1:48

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