Metamath Proof Explorer

Theorem bj-sblem

Description: Lemma for substitution. (Contributed by BJ, 23-Jul-2023)

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

Proof

Step Hyp Ref Expression
1 pm5.74 ⊢ φ → ψ ↔ χ ↔ φ → ψ ↔ φ → χ
2 1 albii ⊢ ∀ x φ → ψ ↔ χ ↔ ∀ x φ → ψ ↔ φ → χ
3 albi ⊢ ∀ x φ → ψ ↔ φ → χ → ∀ x φ → ψ ↔ ∀ x φ → χ
4 2 3 sylbi ⊢ ∀ x φ → ψ ↔ χ → ∀ x φ → ψ ↔ ∀ x φ → χ
5 19.23v ⊢ ∀ x φ → χ ↔ ∃ x φ → χ
6 4 5 bitrdi ⊢ ∀ x φ → ψ ↔ χ → ∀ x φ → ψ ↔ ∃ x φ → χ