Theorem moanmo
Nested at-most-one quantifiers. (Contributed by NM, 25-Jan-2006.)
Conclusion
\( \vdash \exists^\ast x \, (\varphi \wedge \exists^\ast x \, \varphi) \)
Proof
l0
id
\( \vdash \exists^\ast x \, \varphi \rightarrow \exists^\ast x \, \varphi \)
nfmo1
moanim _
\( \vdash \exists^\ast x \, (\exists^\ast x \, \varphi \wedge \varphi) \leftrightarrow \exists^\ast x \, \varphi \rightarrow \exists^\ast x \, \varphi \)
l3
mpbir l0 _
\( \vdash \exists^\ast x \, (\exists^\ast x \, \varphi \wedge \varphi) \)
ancom
mobii _
\( \vdash \exists^\ast x \, (\varphi \wedge \exists^\ast x \, \varphi) \leftrightarrow \exists^\ast x \, (\exists^\ast x \, \varphi \wedge \varphi) \)
mpbir l3 _