theorem Th48: :: LTLAXIO1:48

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