Theorem eqcomd 2237

Description: Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)

Hypothesis

Ref	Expression
eqcomd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
eqcomd	|- ( ph -> B = A )

Proof of Theorem eqcomd

Step	Hyp	Ref	Expression
1		eqcomd.1	. 2 |- ( ph -> A = B )
2		eqcom 2233	. 2 |- ( A = B <-> B = A )
3	1, 2	sylib 122	1 |- ( ph -> B = A )

Syntax hints:   -> wi 4   = wceq 1397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  eqtr2d  2265  eqtr3d  2266  eqtr4d  2267  eqtr2id  2277  eqtr2di  2281  sylan9req  2285  eqeltrrd  2309  eleqtrrd  2311  eleqtrrid  2321  eqeltrrdi  2323  eqnetrrd  2428  neeqtrrd  2432  rspcedeq2vd  2920  dedhb  2975  eqsstrrd  3264  sseqtrrd  3266  eqsstrrdi  3280  dfrab3ss  3485  uneqdifeqim  3580  ifbothdadc  3639  ifbothdc  3640  2if2dc  3645  disjsn2  3732  diftpsn3  3814  elpr2elpr  3859  dfopg  3860  unimax  3927  sndisj  4084  eqbrtrrd  4112  breqtrrd  4116  breqtrrid  4126  eqbrtrrdi  4128  class2seteq  4253  opth1  4328  euotd  4347  opelopabsb  4354  tfisi  4685  0nelxp  4753  opeliunxp  4781  euiotaex  5303  iota4  5306  iotam  5318  fun2ssres  5370  funimass1  5407  funssfv  5665  fnimapr  5706  fvun1  5712  fvco4  5718  elfvmptrab  5742  fmptco  5813  fncofn  5831  foima2  5891  foeqcnvco  5930  f1eqcocnv  5931  f1oiso2  5967  riotass2  5999  riotass  6000  f1ocnvfv3  6006  fvmpopr2d  6157  caovlem2d  6214  f1opw2  6228  offveq  6255  sbcopeq1a  6349  csbopeq1a  6350  eloprabi  6360  cnvf1olem  6388  f2ndf  6390  smoiso  6467  nnaword  6678  eqer  6733  uniqs  6761  mapsncnv  6863  ixpiinm  6892  mapsnf1o  6905  ssenen  7036  findcard2  7077  findcard2s  7078  unsnfidcex  7111  fisseneq  7126  phpeqd  7127  en1eqsn  7146  sbthlemi6  7160  updjud  7280  omp1eomlem  7292  nnnninf2  7325  nninfisollem0  7328  nninfisollemeq  7330  fodju0  7345  3nsssucpw1  7453  enq0sym  7651  enq0tr  7653  recexgt0sr  7992  caucvgsrlemoffcau  8017  axcaucvglemval  8116  le2tri3i  8287  cnegexlem2  8354  nnpcan  8401  addlsub  8548  negf1o  8560  subdi  8563  rereim  8765  cru  8781  divmulassap  8874  divmulasscomap  8875  divap1d  8980  subhalfhalf  9378  div4p1lem1div2  9397  difgtsumgt  9548  elz2  9550  zindd  9597  qapne  9872  divge1  9957  xrlttri3  10031  fseq1p1m1  10328  fzrevral  10339  nn0disj  10372  fzo0addel  10432  fzosplitsnm1  10453  fzosplitprm1  10479  flqlelt  10535  divfl0  10555  flqpmodeq  10588  zmodidfzo  10614  modqmuladd  10627  qnegmod  10630  addmodid  10633  modifeq2int  10647  modqeqmodmin  10655  modfzo0difsn  10656  modsumfzodifsn  10657  addmodlteq  10659  frecuzrdgsuc  10675  frecfzen2  10688  iseqf1olemab  10763  iseqf1olemmo  10766  seqf1oglem1  10780  seqf1oglem2  10781  ser3sub  10784  expgt1  10838  leexp2r  10854  sqoddm1div8  10954  mulsubdivbinom2ap  10972  bcm1k  11021  bcn2m1  11030  hashinfuni  11038  hashennnuni  11040  hashennn  11041  hashunlem  11066  hashprg  11071  fihashssdif  11081  zfz1isolem1  11103  elovmpowrd  11154  ccatsymb  11178  ccatlid  11182  eqs1  11204  ccatw2s1p1g  11221  swrdfv2  11243  swrds1  11248  swrdlsw  11249  pfxfv  11264  swrdswrd  11285  swrdpfx  11287  pfxpfx  11288  pfxlswccat  11293  ccats1pfxeq  11294  wrdind  11302  wrd2ind  11303  pfxccatin12lem1  11308  pfxccatin12lem2  11311  swrdccat3blem  11319  swrdccat3b  11320  ccats1pfxeqbi  11322  reuccatpfxs1lem  11326  reuccatpfxs1  11327  shftlem  11376  shftfvalg  11378  shftfval  11381  replim  11419  cjexp  11453  resqrexlemcalc1  11574  resqrexlemcvg  11579  rersqrtthlem  11590  abssq  11641  recan  11669  negfi  11788  minclpr  11797  mingeb  11802  xrmaxiflemcom  11809  xrmineqinf  11829  xrminltinf  11832  xrminadd  11835  climmpt  11860  climrecl  11884  fsum3cvg  11938  summodclem3  11940  summodclem2a  11941  modfsummodlemstep  12017  isumsplit  12051  arisum  12058  geosergap  12066  geo2sum  12074  mertenslemi1  12095  mertenslem2  12096  clim2divap  12100  fproddccvg  12132  fprodssdc  12150  fprodabs  12176  fproddivapf  12191  fprodmodd  12201  efcj  12233  efsub  12241  eflegeo  12261  sinneg  12286  cosneg  12287  sin01bnd  12317  cos01bnd  12318  modm1div  12360  summodnegmod  12382  dvdseq  12408  addmodlteqALT  12419  mulmoddvds  12423  zob  12451  nn0ob  12468  divalgmod  12487  flodddiv4  12496  bitsinv1  12522  divgcdnnr  12546  gcdneg  12552  bezoutlemsup  12579  dvdssq  12601  lcmneg  12645  3lcm2e6woprm  12657  6lcm4e12  12658  divgcdcoprmex  12673  cncongr1  12674  cncongrcoprm  12677  oddpwdclemxy  12740  oddpwdclemodd  12743  divnumden  12767  zgcdsq  12772  phibnd  12788  hashgcdlem  12809  vfermltl  12823  powm2modprm  12824  reumodprminv  12825  pythagtriplem19  12854  pcprendvds2  12863  pczpre  12869  dvdsprmpweqle  12909  difsqpwdvds  12910  4sqlem4  12964  ennnfonelemex  13034  strndxid  13109  topnvalg  13333  prdssca  13357  intopsn  13449  ismgmid2  13462  mgmidsssn0  13466  gsumfzval  13473  gsumprval  13481  mndpfo  13520  mndfo  13521  mndinvmod  13527  prds0g  13531  mnd1id  13538  mhmf1o  13552  0mhm  13568  gsumwmhm  13580  grpidd2  13623  grpinvid2  13635  grpidssd  13658  grpnpcan  13674  grpsubsub4  13675  qusgrp2  13699  mulginvcom  13733  grpissubg  13780  quselbasg  13816  qus0  13821  ecqusaddd  13824  ghmid  13835  ghminv  13836  imasabl  13922  gsumfzmhm  13929  mgpress  13943  rnglz  13957  rngrz  13958  rngmneg1  13959  rngmneg2  13960  rngpropd  13967  srg1zr  13999  srgmulgass  14001  srgpcomp  14002  srgpcomppsc  14004  ringadd2  14039  ringo2times  14040  ringlz  14055  ringrz  14056  ringinvnzdiv  14062  ringnegl  14063  ringnegr  14064  imasring  14076  qusring2  14078  crngunit  14124  rhmopp  14189  lringuplu  14209  opprdomnbg  14287  lmod0vs  14334  lmodvsmmulgdi  14336  lmodfopne  14339  islss3  14392  lspsn  14429  lmodindp1  14441  rnglidlmmgm  14509  rnglidlmsgrp  14510  rnglidlrng  14511  isridl  14517  zringinvg  14617  zndvds  14662  znf1o  14664  psrgrp  14698  toponcom  14750  tgtopon  14789  restopnb  14904  cnptoprest  14962  blfvalps  15108  bdmopn  15227  cnmet  15253  mpomulcn  15289  limcdifap  15385  dvidsslem  15416  dviaddf  15428  dvexp  15434  dvply2g  15489  coseq0negpitopi  15559  abssinper  15569  rplogbzexp  15677  dvdsppwf1o  15712  mpodvdsmulf1o  15713  fsumdvdsmul  15714  sgmmul  15719  perfect  15724  lgsvalmod  15747  lgsneg  15752  gausslemma2dlem1a  15786  gausslemma2dlem6  15795  gausslemma2dlem7  15796  gausslemma2d  15797  lgsquadlem2  15806  2lgslem1a1  15814  2lgslem1a  15816  2lgslem3c  15823  2lgslem3d  15824  2lgslem3d1  15828  2lgs  15832  2lgsoddprm  15841  uhgrun  15936  upgrun  15976  umgrun  15978  ushgredgedg  16076  issubgr2  16108  uhgrissubgr  16111  subgruhgredgdm  16120  subumgredg2en  16121  subupgr  16123  p1evtxdeqfilem  16161  wlklenvm1  16191  wlklenvm1g  16192  wlkl1loop  16208  upgriswlkdc  16210  uspgr2wlkeq  16215  uspgr2wlkeq2  16216  uspgr2wlkeqi  16217  wlkres  16229  loopclwwlkn1b  16269  clwwlkn1loopb  16270  clwwlkext2edg  16272  clwwlknonccat  16283  s2elclwwlknon2  16286  clwwlknonex2lem2  16288  clwwlknun  16291  subctctexmid  16601  cvgcmp2nlemabs  16636  trilpolemlt1  16645  gsumgfsumlem  16683