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	$$⊢\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\underset{\dot{}}{[}B/b\underset{\dot{}}{]}\underset{\dot{}}{[}C/c\underset{\dot{}}{]}\underset{\dot{}}{[}D/d\underset{\dot{}}{]}\underset{\dot{}}{[}E/e\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}B/b\underset{\dot{}}{]}\underset{\dot{}}{[}C/c\underset{\dot{}}{]}\underset{\dot{}}{[}D/d\underset{\dot{}}{]}\underset{\dot{}}{[}E/e\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbcrot3	$$⊢\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\underset{\dot{}}{[}B/b\underset{\dot{}}{]}\underset{\dot{}}{[}C/c\underset{\dot{}}{]}\underset{\dot{}}{[}D/d\underset{\dot{}}{]}\underset{\dot{}}{[}E/e\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}B/b\underset{\dot{}}{]}\underset{\dot{}}{[}C/c\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\underset{\dot{}}{[}D/d\underset{\dot{}}{]}\underset{\dot{}}{[}E/e\underset{\dot{}}{]}\phi$$
2		sbcrot3	$$⊢\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\underset{\dot{}}{[}D/d\underset{\dot{}}{]}\underset{\dot{}}{[}E/e\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}D/d\underset{\dot{}}{]}\underset{\dot{}}{[}E/e\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi$$
3	2	sbcbii	$$⊢\underset{\dot{}}{[}C/c\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\underset{\dot{}}{[}D/d\underset{\dot{}}{]}\underset{\dot{}}{[}E/e\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/c\underset{\dot{}}{]}\underset{\dot{}}{[}D/d\underset{\dot{}}{]}\underset{\dot{}}{[}E/e\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi$$
4	3	sbcbii	$$⊢\underset{\dot{}}{[}B/b\underset{\dot{}}{]}\underset{\dot{}}{[}C/c\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\underset{\dot{}}{[}D/d\underset{\dot{}}{]}\underset{\dot{}}{[}E/e\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}B/b\underset{\dot{}}{]}\underset{\dot{}}{[}C/c\underset{\dot{}}{]}\underset{\dot{}}{[}D/d\underset{\dot{}}{]}\underset{\dot{}}{[}E/e\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi$$
5	1 4	bitri	$$⊢\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\underset{\dot{}}{[}B/b\underset{\dot{}}{]}\underset{\dot{}}{[}C/c\underset{\dot{}}{]}\underset{\dot{}}{[}D/d\underset{\dot{}}{]}\underset{\dot{}}{[}E/e\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}B/b\underset{\dot{}}{]}\underset{\dot{}}{[}C/c\underset{\dot{}}{]}\underset{\dot{}}{[}D/d\underset{\dot{}}{]}\underset{\dot{}}{[}E/e\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi$$