theorem Th54: :: LTLAXIO2:54

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