Metamath Proof Explorer

Theorem bj-cbv3ta

Description: Closed form of cbv3 . (Contributed by BJ, 2-May-2019)

Ref Expression
Assertion bj-cbv3ta ⊢ ∀ x ∀ y x = y → φ → ψ → ∀ y ∃ x ψ → ψ ∧ ∀ x φ → ∀ y φ → ∀ x φ → ∀ y ψ

Proof

Step Hyp Ref Expression
1 bj-spimt2 ⊢ ∀ x x = y → φ → ψ → ∃ x ψ → ψ → ∀ x φ → ψ
2 1 imp ⊢ ∀ x x = y → φ → ψ ∧ ∃ x ψ → ψ → ∀ x φ → ψ
3 2 alanimi ⊢ ∀ y ∀ x x = y → φ → ψ ∧ ∀ y ∃ x ψ → ψ → ∀ y ∀ x φ → ψ
4 bj-hbalt ⊢ ∀ x φ → ∀ y φ → ∀ x φ → ∀ y ∀ x φ
5 sylgt ⊢ ∀ y ∀ x φ → ψ → ∀ x φ → ∀ y ∀ x φ → ∀ x φ → ∀ y ψ
6 3 4 5 syl2im ⊢ ∀ y ∀ x x = y → φ → ψ ∧ ∀ y ∃ x ψ → ψ → ∀ x φ → ∀ y φ → ∀ x φ → ∀ y ψ
7 6 expimpd ⊢ ∀ y ∀ x x = y → φ → ψ → ∀ y ∃ x ψ → ψ ∧ ∀ x φ → ∀ y φ → ∀ x φ → ∀ y ψ
8 7 alcoms ⊢ ∀ x ∀ y x = y → φ → ψ → ∀ y ∃ x ψ → ψ ∧ ∀ x φ → ∀ y φ → ∀ x φ → ∀ y ψ