Metamath Proof Explorer


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 [˙A / a]˙ [˙B / b]˙ [˙C / c]˙ [˙D / d]˙ [˙E / e]˙ φ [˙B / b]˙ [˙C / c]˙ [˙D / d]˙ [˙E / e]˙ [˙A / a]˙ φ

Proof

Step Hyp Ref Expression
1 sbcrot3 [˙A / a]˙ [˙B / b]˙ [˙C / c]˙ [˙D / d]˙ [˙E / e]˙ φ [˙B / b]˙ [˙C / c]˙ [˙A / a]˙ [˙D / d]˙ [˙E / e]˙ φ
2 sbcrot3 [˙A / a]˙ [˙D / d]˙ [˙E / e]˙ φ [˙D / d]˙ [˙E / e]˙ [˙A / a]˙ φ
3 2 sbcbii [˙C / c]˙ [˙A / a]˙ [˙D / d]˙ [˙E / e]˙ φ [˙C / c]˙ [˙D / d]˙ [˙E / e]˙ [˙A / a]˙ φ
4 3 sbcbii [˙B / b]˙ [˙C / c]˙ [˙A / a]˙ [˙D / d]˙ [˙E / e]˙ φ [˙B / b]˙ [˙C / c]˙ [˙D / d]˙ [˙E / e]˙ [˙A / a]˙ φ
5 1 4 bitri [˙A / a]˙ [˙B / b]˙ [˙C / c]˙ [˙D / d]˙ [˙E / e]˙ φ [˙B / b]˙ [˙C / c]˙ [˙D / d]˙ [˙E / e]˙ [˙A / a]˙ φ