Metamath Proof Explorer

Theorem 19.41

Description: Theorem 19.41 of Margaris p. 90. See 19.41v for a version requiring fewer axioms. (Contributed by NM, 14-May-1993) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 12-Jan-2018)

Ref Expression
Hypothesis 19.41.1 ⊢ Ⅎ x ψ
Assertion 19.41 ⊢ ∃ x φ ∧ ψ ↔ ∃ x φ ∧ ψ

Proof

Step Hyp Ref Expression
1 19.41.1 ⊢ Ⅎ x ψ
2 19.40 ⊢ ∃ x φ ∧ ψ → ∃ x φ ∧ ∃ x ψ
3 1 19.9 ⊢ ∃ x ψ ↔ ψ
4 3 anbi2i ⊢ ∃ x φ ∧ ∃ x ψ ↔ ∃ x φ ∧ ψ
5 2 4 sylib ⊢ ∃ x φ ∧ ψ → ∃ x φ ∧ ψ
6 pm3.21 ⊢ ψ → φ → φ ∧ ψ
7 1 6 eximd ⊢ ψ → ∃ x φ → ∃ x φ ∧ ψ
8 7 impcom ⊢ ∃ x φ ∧ ψ → ∃ x φ ∧ ψ
9 5 8 impbii ⊢ ∃ x φ ∧ ψ ↔ ∃ x φ ∧ ψ