Metamath Proof Explorer

Theorem bj-biexal3

Description: When ph is substituted for ps , both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019)

Ref Expression
Assertion bj-biexal3 ⊢ ∀ x φ → ∀ x ψ ↔ ∀ x ∃ x φ → ψ

Proof

Step Hyp Ref Expression
1 bj-biexal1 ⊢ ∀ x φ → ∀ x ψ ↔ ∃ x φ → ∀ x ψ
2 bj-biexal2 ⊢ ∀ x ∃ x φ → ψ ↔ ∃ x φ → ∀ x ψ
3 1 2 bitr4i ⊢ ∀ x φ → ∀ x ψ ↔ ∀ x ∃ x φ → ψ