Metamath Proof Explorer


Theorem sbidd

Description: An identity theorem for substitution. See sbid . See Remark 9.1 in Megill p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017)

Ref Expression
Hypothesis sbidd.1 φxxψ
Assertion sbidd φψ

Proof

Step Hyp Ref Expression
1 sbidd.1 φxxψ
2 sbid xxψψ
3 1 2 sylib φψ