While you're absolutely right that this is a kind of distributivity, conventionally + is related to "or", * to "and", and ^ to "implies". So the theorem as given would be rendered as something more like "(p + r)^(p + q) implies (p + r^q)".
(The truth table of implication is clearly different from binary exxponentiation)
irb(main):001:0> 0**0
=> 1
irb(main):002:0> 0**1
=> 0
irb(main):003:0> 1**0
=> 1
irb(main):004:0> 1**1
=> 1