theorem Th35: :: HILBERT1:35

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