Theorem sbcom4

Commutativity law for substitution. This theorem was incorrectly used as our previous version of pm11.07 but may still be useful. (Contributed by Andrew Salmon, 17-Jun-2011.) (Proof shortened by Jim Kingdon, 22-Jan-2018.)

Conclusion
\( \vdash [ w' / x ] \, [ y' / z ] \, \varphi \leftrightarrow [ y' / x ] \, [ w' / z ] \, \varphi \)
Proof
l0
sbv
\( \vdash [ w' / x ] \, \varphi \leftrightarrow \varphi \)
sbv
l2
sbbii _
\( \vdash [ w' / x ] \, [ y' / z ] \, \varphi \leftrightarrow [ w' / x ] \, \varphi \)
sbv
l4
sbbii _
\( \vdash [ y' / x ] \, [ w' / z ] \, \varphi \leftrightarrow [ y' / x ] \, \varphi \)
sbv
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \varphi \)
bitri l4 _
\( \vdash [ y' / x ] \, [ w' / z ] \, \varphi \leftrightarrow \varphi \)
3bitr4i l0 l2 _