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 φ χ