Theorem sbcom
A commutativity law for substitution. Usage of this theorem is
discouraged because it depends on [ax-13]. Check out sbcom3vv for a
version requiring fewer axioms. (Contributed by NM, 27-May-1997.) (Proof
shortened by Wolf Lammen, 20-Sep-2018.) (New usage is discouraged.)
Conclusion
\( \vdash [ y' / z ] \, [ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, [ y' / z ] \, \varphi \)
Proof
l0
sbco3
\( \vdash [ y' / z ] \, [ z / x ] \, \varphi \leftrightarrow [ y' / x ] \, [ x / z ] \, \varphi \)
l1
sbcom3
\( \vdash [ y' / z ] \, [ z / x ] \, \varphi \leftrightarrow [ y' / z ] \, [ y' / x ] \, \varphi \)
sbcom3
\( \vdash [ y' / x ] \, [ x / z ] \, \varphi \leftrightarrow [ y' / x ] \, [ y' / z ] \, \varphi \)
3bitr3i l0 l1 _