Metamath Proof Explorer

Theorem bj-pm11.53vw

Description: Version of pm11.53v with nonfreeness antecedents. One can also prove the theorem with antecedent ( F// y A. x ph /\ A. y F// x ps ) . (Contributed by BJ, 7-Oct-2024)

Ref Expression
Assertion bj-pm11.53vw ⊢ ∀ x Ⅎ' y φ ∧ Ⅎ' x ∀ y ψ → ∀ x ∀ y φ → ψ ↔ ∃ x φ → ∀ y ψ

Proof

Step Hyp Ref Expression
1 simpl ⊢ ∀ x Ⅎ' y φ ∧ Ⅎ' x ∀ y ψ → ∀ x Ⅎ' y φ
2 bj-19.21t ⊢ Ⅎ' y φ → ∀ y φ → ψ ↔ φ → ∀ y ψ
3 1 2 sylg ⊢ ∀ x Ⅎ' y φ ∧ Ⅎ' x ∀ y ψ → ∀ x ∀ y φ → ψ ↔ φ → ∀ y ψ
4 albi ⊢ ∀ x ∀ y φ → ψ ↔ φ → ∀ y ψ → ∀ x ∀ y φ → ψ ↔ ∀ x φ → ∀ y ψ
5 3 4 syl ⊢ ∀ x Ⅎ' y φ ∧ Ⅎ' x ∀ y ψ → ∀ x ∀ y φ → ψ ↔ ∀ x φ → ∀ y ψ
6 bj-19.23t ⊢ Ⅎ' x ∀ y ψ → ∀ x φ → ∀ y ψ ↔ ∃ x φ → ∀ y ψ
7 6 adantl ⊢ ∀ x Ⅎ' y φ ∧ Ⅎ' x ∀ y ψ → ∀ x φ → ∀ y ψ ↔ ∃ x φ → ∀ y ψ
8 5 7 bitrd ⊢ ∀ x Ⅎ' y φ ∧ Ⅎ' x ∀ y ψ → ∀ x ∀ y φ → ψ ↔ ∃ x φ → ∀ y ψ