Theorem anim12ci 567

Description: Variant of anim12i 566 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
anim12i.1
anim12i.2

Assertion

Ref	Expression
anim12ci

Proof of Theorem anim12ci

Step	Hyp	Ref	Expression
1		anim12i.2	. . 3
2		anim12i.1	. . 3
3	1, 2	anim12i 566	. 2
4	3	ancoms 453	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  2exeu  2371  dfco2a  5512  fliftval  6214  omlimcl  7246  funsnfsupp  7873  supmaxlemOLD  7945  ltrnq  9378  ltsrpr  9475  difelfznle  11818  swrdspsleq  12673  swrdccatin12lem2a  12710  repswswrd  12756  cshwidxm  12778  modprm0  14330  brssc  15183  resmhm  15990  mhmco  15993  gasubg  16340  idrespermg  16436  rhmco  17386  resrhm  17458  cply1mul  18335  dmatmul  18999  scmatf1  19033  slesolinv  19182  slesolinvbi  19183  slesolex  19184  cramerimplem3  19187  cramerimp  19188  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  bwth  19910  nmhmco  21263  chpchtsum  23494  dchrisum0lem1  23701  wlkdvspthlem  24609  clwlkisclwwlklem0  24788  clwwlkf1  24796  wwlksubclwwlk  24804  clwlkfclwwlk  24844  clwlkf1clwwlklem  24849  vdgrf  24898  frgra3v  25002  frgrancvvdeqlem3  25032  frghash2spot  25063  numclwwlk3  25109  numclwwlk5  25112  frgrareg  25117  occon2  26206  itgspltprt  31778  2rexreu  32190  resmgmhm  32486  mgmhmco  32489  rnghmco  32713  ztprmneprm  32936  nn0sumltlt  32939  ldepspr  33074  aacllem  33216  bnj1110  34038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371