Add phimullem to iset.mm
Add phimullem to iset.mm

The theorem is stated as in set.mm. The proof is basically the set.mm
one but needs to be changed in various places for different closure
theorems or decidability.

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