∃1→∃mo
Theorem.
Arguments:
(sv),
(pr),
Assertions:
(
)
Proof:
Hyp
Ref
Line
Expr
df-∃1-alt5
1
(
(
))
1
siman>
2
(
)