Add exmidexmid to iset.mm
Add exmidexmid to iset.mm

This is the key theorem in terms of going from EXMID to a propositional
version of excluded middle. It is proved much like undifexmid or a bunch
of similar theorems we already have.

metamath/set.mm,metamath/set.mm,metamath/set.mm