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 \leftrightarrow \left[y/x\right]\left[w/z\right]\phi$$

Proof

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