Description: Obsolete proof of sbiev as of 18-Jul-2023. (Contributed by Wolf Lammen, 18-Jan-2023) (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sbiev.1 | |- F/ x ps |
|
sbiev.2 | |- ( x = y -> ( ph <-> ps ) ) |
||
Assertion | sbievOLD | |- ( [ y / x ] ph <-> ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbiev.1 | |- F/ x ps |
|
2 | sbiev.2 | |- ( x = y -> ( ph <-> ps ) ) |
|
3 | equsb1v | |- [ y / x ] x = y |
|
4 | 2 | sbimi | |- ( [ y / x ] x = y -> [ y / x ] ( ph <-> ps ) ) |
5 | 3 4 | ax-mp | |- [ y / x ] ( ph <-> ps ) |
6 | 1 | sbf | |- ( [ y / x ] ps <-> ps ) |
7 | 6 | sblbisvOLD | |- ( [ y / x ] ( ph <-> ps ) <-> ( [ y / x ] ph <-> ps ) ) |
8 | 5 7 | mpbi | |- ( [ y / x ] ph <-> ps ) |