Metamath Proof Explorer

Theorem bj-sblem1

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

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

Proof

Step Hyp Ref Expression
1 ax-2 ⊢ φ → ψ → χ → φ → ψ → φ → χ
2 1 al2imi ⊢ ∀ x φ → ψ → χ → ∀ x φ → ψ → ∀ x φ → χ
3 19.23v ⊢ ∀ x φ → χ ↔ ∃ x φ → χ
4 2 3 imbitrdi ⊢ ∀ x φ → ψ → χ → ∀ x φ → ψ → ∃ x φ → χ