Description: Conversion of double implicit substitution to explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . See 2sbievw for a version with extra disjoint variables, but based on fewer axioms. (Contributed by AV, 29-Jul-2023) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 2sbiev.1 | |- ( ( x = t /\ y = u ) -> ( ph <-> ps ) ) |
|
Assertion | 2sbiev | |- ( [ t / x ] [ u / y ] ph <-> ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2sbiev.1 | |- ( ( x = t /\ y = u ) -> ( ph <-> ps ) ) |
|
2 | nfv | |- F/ x ps |
|
3 | 1 | sbiedv | |- ( x = t -> ( [ u / y ] ph <-> ps ) ) |
4 | 2 3 | sbie | |- ( [ t / x ] [ u / y ] ph <-> ps ) |