MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  caov12 Unicode version

Theorem caov12 6261
Description: Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
Hypotheses
Ref Expression
caov.1
caov.2
caov.3
caov.com
caov.ass
Assertion
Ref Expression
caov12
Distinct variable groups:   , , ,   , , ,   , , ,   , , ,

Proof of Theorem caov12
StepHypRef Expression
1 caov.1 . . . 4
2 caov.2 . . . 4
3 caov.com . . . 4
41, 2, 3caovcom 6230 . . 3
54oveq1i 6071 . 2
6 caov.3 . . 3
7 caov.ass . . 3
81, 2, 6, 7caovass 6233 . 2
92, 1, 6, 7caovass 6233 . 2
105, 8, 93eqtr3i 2450 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1687  e.wcel 1749   cvv 2951  (class class class)co 6061
This theorem is referenced by:  caov31  6262  caov4  6264  caovmo  6270  distrnq  9076  ltaddnq  9089  ltexnq  9090  1idpr  9144  prlem934  9148  prlem936  9162  mulcmpblnrlem  9186  ltsosr  9207  0idsr  9210  1idsr  9211  recexsrlem  9216  mulgt0sr  9218  axmulass  9270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ral 2699  df-rex 2700  df-rab 2703  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-uni 4067  df-br 4268  df-iota 5353  df-fv 5398  df-ov 6064
  Copyright terms: Public domain W3C validator