This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ψ

Proof

Step Hyp Ref Expression
1 ibar ⊢ φ → ψ ↔ φ ∧ ψ
2 1 mobidv ⊢ φ → ∃* x ψ ↔ ∃* x φ ∧ ψ
3 simpl ⊢ φ ∧ ψ → φ
4 3 exlimiv ⊢ ∃ x φ ∧ ψ → φ
5 2 4 moanimlem ⊢ ∃* x φ ∧ ψ ↔ φ → ∃* x ψ