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

Metamath Proof Explorer

Theorem bj-19.41t

Description: Closed form of 19.41 from the same axioms as 19.41v . The same is doable with 19.27 , 19.28 , 19.31 , 19.32 , 19.44 , 19.45 . (Contributed by BJ, 2-Dec-2023)

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

Proof

Step Hyp Ref Expression
1 exancom ⊢ ∃ x φ ∧ ψ ↔ ∃ x ψ ∧ φ
2 bj-19.42t ⊢ Ⅎ' x ψ → ∃ x ψ ∧ φ ↔ ψ ∧ ∃ x φ
3 1 2 bitrid ⊢ Ⅎ' x ψ → ∃ x φ ∧ ψ ↔ ψ ∧ ∃ x φ
4 3 biancomd ⊢ Ⅎ' x ψ → ∃ x φ ∧ ψ ↔ ∃ x φ ∧ ψ