Metamath Proof Explorer


Theorem 2sbievw

Description: Conversion of double implicit substitution to explicit substitution. Version of 2sbiev with more disjoint variable conditions, requiring fewer axioms. (Contributed by AV, 29-Jul-2023) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypothesis 2sbievw.1
|- ( ( x = t /\ y = u ) -> ( ph <-> ps ) )
Assertion 2sbievw
|- ( [ t / x ] [ u / y ] ph <-> ps )

Proof

Step Hyp Ref Expression
1 2sbievw.1
 |-  ( ( x = t /\ y = u ) -> ( ph <-> ps ) )
2 1 sbiedvw
 |-  ( x = t -> ( [ u / y ] ph <-> ps ) )
3 2 sbievw
 |-  ( [ t / x ] [ u / y ] ph <-> ps )