theorem Th47: :: LTLAXIO2:47

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