Remove difcom and consequences from iset.mm
Remove difcom and consequences from iset.mm

This is difcom, pssdifcom1, and pssdifcom2.  The proofs are not
intuitionistic, it doesn't seem like these should be theorems
of intuitionistic logic (because they boil down to con1,
basically), and there aren't obvious intuitionistic analogues.

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