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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-ax12 | ||
2 | pm3.31 | ||
3 | 2 | aleximi | |
4 | 1 3 | ax-mp | |
5 | hbe1a | ||
6 | 4 5 | syl | |
7 | equs4v | ||
8 | 6 7 | impbii |