Metamath Proof Explorer


Theorem caov12

Description: Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995)

Ref Expression
Hypotheses caov.1 AV
caov.2 BV
caov.3 CV
caov.com xFy=yFx
caov.ass xFyFz=xFyFz
Assertion caov12 AFBFC=BFAFC

Proof

Step Hyp Ref Expression
1 caov.1 AV
2 caov.2 BV
3 caov.3 CV
4 caov.com xFy=yFx
5 caov.ass xFyFz=xFyFz
6 1 2 4 caovcom AFB=BFA
7 6 oveq1i AFBFC=BFAFC
8 1 2 3 5 caovass AFBFC=AFBFC
9 2 1 3 5 caovass BFAFC=BFAFC
10 7 8 9 3eqtr3i AFBFC=BFAFC