Metamath Proof Explorer

Theorem 19.41v

Description: Version of 19.41 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993) Remove dependency on ax-6 . (Revised by Rohan Ridenour, 15-Apr-2022)

Ref Expression
Assertion 19.41v ⊢ ∃ x φ ∧ ψ ↔ ∃ x φ ∧ ψ

Proof

Step Hyp Ref Expression
1 19.40 ⊢ ∃ x φ ∧ ψ → ∃ x φ ∧ ∃ x ψ
2 ax5e ⊢ ∃ x ψ → ψ
3 2 anim2i ⊢ ∃ x φ ∧ ∃ x ψ → ∃ x φ ∧ ψ
4 1 3 syl ⊢ ∃ x φ ∧ ψ → ∃ x φ ∧ ψ
5 pm3.21 ⊢ ψ → φ → φ ∧ ψ
6 5 eximdv ⊢ ψ → ∃ x φ → ∃ x φ ∧ ψ
7 6 impcom ⊢ ∃ x φ ∧ ψ → ∃ x φ ∧ ψ
8 4 7 impbii ⊢ ∃ x φ ∧ ψ ↔ ∃ x φ ∧ ψ