Metamath Proof Explorer

Theorem moanimv

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim requiring disjoint variables, but fewer axioms. (Contributed by NM, 23-Mar-1995) Reduce axiom usage . (Revised by Wolf Lammen, 8-Feb-2023)

Ref Expression
Assertion moanimv * x φ ψ φ * x ψ


Step Hyp Ref Expression
1 ibar φ ψ φ ψ
2 1 mobidv φ * x ψ * x φ ψ
3 simpl φ ψ φ
4 3 exlimiv x φ ψ φ
5 2 4 moanimlem * x φ ψ φ * x ψ