theorem Th45: :: LTLAXIO2:45

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