Metamath Proof Explorer

Theorem bj-19.42t

Description: Closed form of 19.42 from the same axioms as 19.42v . (Contributed by BJ, 2-Dec-2023)

Ref Expression
Assertion bj-19.42t ⊢ Ⅎ' x φ → ∃ x φ ∧ ψ ↔ φ ∧ ∃ x ψ

Proof

Step Hyp Ref Expression
1 19.40 ⊢ ∃ x φ ∧ ψ → ∃ x φ ∧ ∃ x ψ
2 bj-nnfe ⊢ Ⅎ' x φ → ∃ x φ → φ
3 2 anim1d ⊢ Ⅎ' x φ → ∃ x φ ∧ ∃ x ψ → φ ∧ ∃ x ψ
4 1 3 syl5 ⊢ Ⅎ' x φ → ∃ x φ ∧ ψ → φ ∧ ∃ x ψ
5 bj-nnfa ⊢ Ⅎ' x φ → φ → ∀ x φ
6 5 anim1d ⊢ Ⅎ' x φ → φ ∧ ∃ x ψ → ∀ x φ ∧ ∃ x ψ
7 19.29 ⊢ ∀ x φ ∧ ∃ x ψ → ∃ x φ ∧ ψ
8 6 7 syl6 ⊢ Ⅎ' x φ → φ ∧ ∃ x ψ → ∃ x φ ∧ ψ
9 4 8 impbid ⊢ Ⅎ' x φ → ∃ x φ ∧ ψ ↔ φ ∧ ∃ x ψ