theorem th16: :: LTLAXIO5:3

for A, B, C being Element of LTLB_WFF holds (A => B) => ((B => C) => (A => C)) is LTL_TAUT_OF_PL