Metamath Proof Explorer


Theorem caov13d

Description: Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995) (Revised by Mario Carneiro, 30-Dec-2014)

Ref Expression
Hypotheses caovd.1 φAS
caovd.2 φBS
caovd.3 φCS
caovd.com φxSySxFy=yFx
caovd.ass φxSySzSxFyFz=xFyFz
Assertion caov13d φAFBFC=CFBFA

Proof

Step Hyp Ref Expression
1 caovd.1 φAS
2 caovd.2 φBS
3 caovd.3 φCS
4 caovd.com φxSySxFy=yFx
5 caovd.ass φxSySzSxFyFz=xFyFz
6 1 2 3 4 5 caov31d φAFBFC=CFBFA
7 5 1 2 3 caovassd φAFBFC=AFBFC
8 5 3 2 1 caovassd φCFBFA=CFBFA
9 6 7 8 3eqtr3d φAFBFC=CFBFA