Metamath Proof Explorer


Theorem bj-subst

Description: Proof of sbalex from core axioms, ax-10 (modal5), and bj-ax12 . (Contributed by BJ, 29-Dec-2020) (Proof modification is discouraged.)

Ref Expression
Assertion bj-subst x x = y φ x x = y φ

Proof

Step Hyp Ref Expression
1 bj-ax12 x x = y φ x x = y φ
2 pm3.31 x = y φ x x = y φ x = y φ x x = y φ
3 2 aleximi x x = y φ x x = y φ x x = y φ x x x = y φ
4 1 3 ax-mp x x = y φ x x x = y φ
5 hbe1a x x x = y φ x x = y φ
6 4 5 syl x x = y φ x x = y φ
7 equs4v x x = y φ x x = y φ
8 6 7 impbii x x = y φ x x = y φ