theorem :: LTLAXIO2:52

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