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	⊢ ( [ 𝑤 / 𝑥 ] [ 𝑦 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbv	⊢ ( [ 𝑤 / 𝑥 ] 𝜑 ↔ 𝜑 )
2		sbv	⊢ ( [ 𝑦 / 𝑧 ] 𝜑 ↔ 𝜑 )
3	2	sbbii	⊢ ( [ 𝑤 / 𝑥 ] [ 𝑦 / 𝑧 ] 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝜑 )
4		sbv	⊢ ( [ 𝑤 / 𝑧 ] 𝜑 ↔ 𝜑 )
5	4	sbbii	⊢ ( [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 )
6		sbv	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 )
7	5 6	bitri	⊢ ( [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ↔ 𝜑 )
8	1 3 7	3bitr4i	⊢ ( [ 𝑤 / 𝑥 ] [ 𝑦 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 )