theorem Th51: :: LTLAXIO1:51

for p, q, r, s being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p => (q => r) & X |- r => s holds
X |- p => (q => s)