theorem Th53: :: LTLAXIO2:53

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