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	|- ( [. A / a ]. [. B / b ]. [. C / c ]. ph <-> [. B / b ]. [. C / c ]. [. A / a ]. ph )

Proof

Step	Hyp	Ref	Expression
1		sbccom	|- ( [. A / a ]. [. B / b ]. [. C / c ]. ph <-> [. B / b ]. [. A / a ]. [. C / c ]. ph )
2		sbccom	|- ( [. A / a ]. [. C / c ]. ph <-> [. C / c ]. [. A / a ]. ph )
3	2	sbcbii	|- ( [. B / b ]. [. A / a ]. [. C / c ]. ph <-> [. B / b ]. [. C / c ]. [. A / a ]. ph )
4	1 3	bitri	|- ( [. A / a ]. [. B / b ]. [. C / c ]. ph <-> [. B / b ]. [. C / c ]. [. A / a ]. ph )