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

Proof

Step Hyp Ref Expression
1 sbcrot3 
 |-  ( [. A / a ]. [. B / b ]. [. C / c ]. [. D / d ]. [. E / e ]. ph <-> [. B / b ]. [. C / c ]. [. A / a ]. [. D / d ]. [. E / e ]. ph )
2 sbcrot3 
 |-  ( [. A / a ]. [. D / d ]. [. E / e ]. ph <-> [. D / d ]. [. E / e ]. [. A / a ]. ph )
3 2 sbcbii 
 |-  ( [. C / c ]. [. A / a ]. [. D / d ]. [. E / e ]. ph <-> [. C / c ]. [. D / d ]. [. E / e ]. [. A / a ]. ph )
4 3 sbcbii 
 |-  ( [. B / b ]. [. C / c ]. [. A / a ]. [. D / d ]. [. E / e ]. ph <-> [. B / b ]. [. C / c ]. [. D / d ]. [. E / e ]. [. A / a ]. ph )
5 1 4 bitri 
 |-  ( [. A / a ]. [. B / b ]. [. C / c ]. [. D / d ]. [. E / e ]. ph <-> [. B / b ]. [. C / c ]. [. D / d ]. [. E / e ]. [. A / a ]. ph )