Metamath Proof Explorer

Theorem 2sbbii

Description: Infer double substitution into both sides of a logical equivalence. (Contributed by AV, 30-Jul-2023)

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

Proof

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