OK, now this result does surprise me. I think I just found a ruleset that is not closed under modus ponens! D10+D12+D13+E:
- validates ~~φ->φ.
- validates (~~φ->φ)->(φv~&phi).
- does not validate φv~φ.
And here are my proofs to double check my work, because this is very, very strange:
In fact, the same also holds of D10+D12+D13, without E: