Theorem sbidm

An idempotent law for substitution. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 30-Jun-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (New usage is discouraged.)

Conclusion
\( \vdash [ y' / x ] \, [ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, \varphi \)
Proof
l0
sbequ12
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow [ y' / x ] \, \varphi) \)
l1
pm5.74i _
l2
sbbii _
\( \vdash [ y' / x ] \, (x = y' \rightarrow \varphi) \leftrightarrow [ y' / x ] \, (x = y' \rightarrow [ y' / x ] \, \varphi) \)
l3
sbequ8
\( \vdash [ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, (x = y' \rightarrow \varphi) \)
l4
sbequ8
\( \vdash [ y' / x ] \, [ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, (x = y' \rightarrow [ y' / x ] \, \varphi) \)
l5
3bitr4ri l2 l3 _