theorem Th15: :: HILBERT1:15

for p, q being Element of HP-WFF st q in HP_TAUT holds
p => q in HP_TAUT