theorem Th46: :: LTLAXIO1:46

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