Theorem sbco3

A composition law for substitution. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 18-Sep-2018.) (New usage is discouraged.)

Conclusion
\( \vdash [ z' / y ] \, [ y / x ] \, \varphi \leftrightarrow [ z' / x ] \, [ x / y ] \, \varphi \)
Proof
l0
sbco
\( \vdash [ y / x ] \, [ x / y ] \, \varphi \leftrightarrow [ y / x ] \, \varphi \)
l1
sbbii _
\( \vdash [ z' / y ] \, [ y / x ] \, [ x / y ] \, \varphi \leftrightarrow [ z' / y ] \, [ y / x ] \, \varphi \)
l2
sbco2vv
\( \vdash [ z' / y ] \, [ y / x ] \, [ x / y ] \, \varphi \leftrightarrow [ z' / x ] \, [ x / y ] \, \varphi \)
l3
bitr3i l1 _