Metamath Proof Explorer


Theorem sbeqi

Description: Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018)

Ref Expression
Assertion sbeqi x=yzφψxzφyzψ

Proof

Step Hyp Ref Expression
1 spsbbi zφψxzφxzψ
2 sbequ x=yxzψyzψ
3 1 2 sylan9bbr x=yzφψxzφyzψ