Theorem sbcrot3

Description: Rotate a sequence of three explicit substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Assertion	sbcrot3	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] 𝜑 ↔ [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] [ 𝐴 / 𝑎 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbccom	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] 𝜑 ↔ [ 𝐵 / 𝑏 ] [ 𝐴 / 𝑎 ] [ 𝐶 / 𝑐 ] 𝜑 )
2		sbccom	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐶 / 𝑐 ] 𝜑 ↔ [ 𝐶 / 𝑐 ] [ 𝐴 / 𝑎 ] 𝜑 )
3	2	sbcbii	⊢ ( [ 𝐵 / 𝑏 ] [ 𝐴 / 𝑎 ] [ 𝐶 / 𝑐 ] 𝜑 ↔ [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] [ 𝐴 / 𝑎 ] 𝜑 )
4	1 3	bitri	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] 𝜑 ↔ [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] [ 𝐴 / 𝑎 ] 𝜑 )