# Metamath Proof Explorer

## Theorem sbcom4

Description: 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)

Ref Expression
Assertion sbcom4 ${⊢}\left[{w}/{x}\right]\left[{y}/{z}\right]{\phi }↔\left[{y}/{x}\right]\left[{w}/{z}\right]{\phi }$

### Proof

Step Hyp Ref Expression
1 sbv ${⊢}\left[{w}/{x}\right]{\phi }↔{\phi }$
2 sbv ${⊢}\left[{y}/{z}\right]{\phi }↔{\phi }$
3 2 sbbii ${⊢}\left[{w}/{x}\right]\left[{y}/{z}\right]{\phi }↔\left[{w}/{x}\right]{\phi }$
4 sbv ${⊢}\left[{w}/{z}\right]{\phi }↔{\phi }$
5 4 sbbii ${⊢}\left[{y}/{x}\right]\left[{w}/{z}\right]{\phi }↔\left[{y}/{x}\right]{\phi }$
6 sbv ${⊢}\left[{y}/{x}\right]{\phi }↔{\phi }$
7 5 6 bitri ${⊢}\left[{y}/{x}\right]\left[{w}/{z}\right]{\phi }↔{\phi }$
8 1 3 7 3bitr4i ${⊢}\left[{w}/{x}\right]\left[{y}/{z}\right]{\phi }↔\left[{y}/{x}\right]\left[{w}/{z}\right]{\phi }$