theorem Th40: :: LTLAXIO2:40

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