∃1→∃mo

Theorem.

Arguments:

x (sv), phi (pr),

Assertions:

(_e1xphito_em1xphi)

Proof:

Hyp Ref Line Expr
df-∃1-alt51(_e1xphito(existsxphiwedge_em1xphi))
1siman>2(_e1xphito_em1xphi)