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

Metamath Proof Explorer

Theorem 19.42v

Description: Version of 19.42 with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993)

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

Proof

Step Hyp Ref Expression
1 19.41v ⊢ ∃ x ψ ∧ φ ↔ ∃ x ψ ∧ φ
2 exancom ⊢ ∃ x φ ∧ ψ ↔ ∃ x ψ ∧ φ
3 ancom ⊢ φ ∧ ∃ x ψ ↔ ∃ x ψ ∧ φ
4 1 2 3 3bitr4i ⊢ ∃ x φ ∧ ψ ↔ φ ∧ ∃ x ψ