Description: Deduction substituting both sides of a biconditional, with ph and x disjoint. See also sbbid . (Contributed by Wolf Lammen, 6-May-2023) (Proof shortened by Steven Nguyen, 6-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | sbbidv.1 | |- ( ph -> ( ps <-> ch ) ) |
|
Assertion | sbbidv | |- ( ph -> ( [ t / x ] ps <-> [ t / x ] ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbbidv.1 | |- ( ph -> ( ps <-> ch ) ) |
|
2 | 1 | alrimiv | |- ( ph -> A. x ( ps <-> ch ) ) |
3 | spsbbi | |- ( A. x ( ps <-> ch ) -> ( [ t / x ] ps <-> [ t / x ] ch ) ) |
|
4 | 2 3 | syl | |- ( ph -> ( [ t / x ] ps <-> [ t / x ] ch ) ) |