theorem Th22: :: HILBERT2:22

for p, q, r, s being Element of HP-WFF holds p '&' q <> r => s