Theorem sbcrot5

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

	Ref	Expression
Assertion	sbcrot5	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] [ 𝐷 / 𝑑 ] [ 𝐸 / 𝑒 ] 𝜑 ↔ [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] [ 𝐷 / 𝑑 ] [ 𝐸 / 𝑒 ] [ 𝐴 / 𝑎 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbcrot3	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] [ 𝐷 / 𝑑 ] [ 𝐸 / 𝑒 ] 𝜑 ↔ [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] [ 𝐴 / 𝑎 ] [ 𝐷 / 𝑑 ] [ 𝐸 / 𝑒 ] 𝜑 )
2		sbcrot3	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐷 / 𝑑 ] [ 𝐸 / 𝑒 ] 𝜑 ↔ [ 𝐷 / 𝑑 ] [ 𝐸 / 𝑒 ] [ 𝐴 / 𝑎 ] 𝜑 )
3	2	sbcbii	⊢ ( [ 𝐶 / 𝑐 ] [ 𝐴 / 𝑎 ] [ 𝐷 / 𝑑 ] [ 𝐸 / 𝑒 ] 𝜑 ↔ [ 𝐶 / 𝑐 ] [ 𝐷 / 𝑑 ] [ 𝐸 / 𝑒 ] [ 𝐴 / 𝑎 ] 𝜑 )
4	3	sbcbii	⊢ ( [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] [ 𝐴 / 𝑎 ] [ 𝐷 / 𝑑 ] [ 𝐸 / 𝑒 ] 𝜑 ↔ [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] [ 𝐷 / 𝑑 ] [ 𝐸 / 𝑒 ] [ 𝐴 / 𝑎 ] 𝜑 )
5	1 4	bitri	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] [ 𝐷 / 𝑑 ] [ 𝐸 / 𝑒 ] 𝜑 ↔ [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] [ 𝐷 / 𝑑 ] [ 𝐸 / 𝑒 ] [ 𝐴 / 𝑎 ] 𝜑 )