Metamath Proof Explorer

Theorem sepnsepolem1

Description: Lemma for sepnsepo . (Contributed by Zhi Wang, 1-Sep-2024)

Ref Expression
Assertion sepnsepolem1 ⊢ ∃ x ∈ J ∃ y ∈ J φ ∧ ψ ∧ χ ↔ ∃ x ∈ J φ ∧ ∃ y ∈ J ψ ∧ χ

Proof

Step Hyp Ref Expression
1 3anass ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
2 1 2rexbii ⊢ ∃ x ∈ J ∃ y ∈ J φ ∧ ψ ∧ χ ↔ ∃ x ∈ J ∃ y ∈ J φ ∧ ψ ∧ χ
3 r19.42v ⊢ ∃ y ∈ J φ ∧ ψ ∧ χ ↔ φ ∧ ∃ y ∈ J ψ ∧ χ
4 3 rexbii ⊢ ∃ x ∈ J ∃ y ∈ J φ ∧ ψ ∧ χ ↔ ∃ x ∈ J φ ∧ ∃ y ∈ J ψ ∧ χ
5 2 4 bitri ⊢ ∃ x ∈ J ∃ y ∈ J φ ∧ ψ ∧ χ ↔ ∃ x ∈ J φ ∧ ∃ y ∈ J ψ ∧ χ