theorem Th1: :: LTLAXIO1:1

for a, b, c being boolean object holds (a => (b '&' c)) => (a => b) = 1