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

Proof

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