theorem Th46: :: LTLAXIO2:46

for p, q, r being Element of LTLB_WFF holds (p => q) => ((p => r) => ((r => p) => (r => q))) is ctaut