Theorem sbco

A composition law for substitution. Usage of this theorem is discouraged because it depends on [ax-13]. See sbcov for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) (New usage is discouraged.)

Conclusion
\( \vdash [ y / x ] \, [ x / y ] \, \varphi \leftrightarrow [ y / x ] \, \varphi \)
Proof
l0
sbcom3
\( \vdash [ y / x ] \, [ x / y ] \, \varphi \leftrightarrow [ y / x ] \, [ y / y ] \, \varphi \)
sbid
sbbii _
\( \vdash [ y / x ] \, [ y / y ] \, \varphi \leftrightarrow [ y / x ] \, \varphi \)
bitri l0 _