theorem th17: :: LTLAXIO5:4

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