theorem Th20: :: HILBERT2:20

for p, q, r, s being Element of HP-WFF st p => q = r => s holds
( p = r & s = q )