Intuitionize iota4an in iset.mm
Intuitionize iota4an in iset.mm

The proof just needs to make use of the E! x ( ph /\ ps )
condition one more place. The statement of the theorem
is unchanged.

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