Metamath Proof Explorer

Theorem 19.42

Description: Theorem 19.42 of Margaris p. 90. See 19.42v for a version requiring fewer axioms. See exan for an immediate version. (Contributed by NM, 18-Aug-1993)

Ref Expression
Hypothesis 19.42.1 ⊢ Ⅎ x φ
Assertion 19.42 ⊢ ∃ x φ ∧ ψ ↔ φ ∧ ∃ x ψ

Proof

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