Theorem eqcomd 2210

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 2206	. 2 |- ( A = B <-> B = A )
3	1, 2	sylib 122	1 |- ( ph -> B = A )

Syntax hints:   -> wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-ext 2186

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

This theorem is referenced by:  eqtr2d  2238  eqtr3d  2239  eqtr4d  2240  eqtr2id  2250  eqtr2di  2254  sylan9req  2258  eqeltrrd  2282  eleqtrrd  2284  eleqtrrid  2294  eqeltrrdi  2296  eqnetrrd  2401  neeqtrrd  2405  rspcedeq2vd  2886  dedhb  2941  eqsstrrd  3229  sseqtrrd  3231  eqsstrrdi  3245  dfrab3ss  3450  uneqdifeqim  3545  ifbothdadc  3603  ifbothdc  3604  disjsn2  3695  diftpsn3  3773  dfopg  3816  unimax  3883  sndisj  4039  eqbrtrrd  4067  breqtrrd  4071  breqtrrid  4081  eqbrtrrdi  4083  class2seteq  4206  opth1  4279  euotd  4298  opelopabsb  4305  tfisi  4634  0nelxp  4702  opeliunxp  4729  euiotaex  5247  iota4  5250  iotam  5262  fun2ssres  5313  funimass1  5350  funssfv  5601  fnimapr  5638  fvun1  5644  fvco4  5650  elfvmptrab  5674  fmptco  5745  foima2  5819  foeqcnvco  5858  f1eqcocnv  5859  f1oiso2  5895  riotass2  5925  riotass  5926  f1ocnvfv3  5932  fvmpopr2d  6081  caovlem2d  6138  f1opw2  6151  offveq  6178  sbcopeq1a  6272  csbopeq1a  6273  eloprabi  6281  cnvf1olem  6309  f2ndf  6311  smoiso  6387  nnaword  6596  eqer  6651  uniqs  6679  mapsncnv  6781  ixpiinm  6810  mapsnf1o  6823  ssenen  6947  findcard2  6985  findcard2s  6986  unsnfidcex  7016  fisseneq  7030  phpeqd  7031  en1eqsn  7049  sbthlemi6  7063  updjud  7183  omp1eomlem  7195  nnnninf2  7228  nninfisollem0  7231  nninfisollemeq  7233  fodju0  7248  3nsssucpw1  7347  enq0sym  7544  enq0tr  7546  recexgt0sr  7885  caucvgsrlemoffcau  7910  axcaucvglemval  8009  le2tri3i  8180  cnegexlem2  8247  nnpcan  8294  addlsub  8441  negf1o  8453  subdi  8456  rereim  8658  cru  8674  divmulassap  8767  divmulasscomap  8768  divap1d  8873  subhalfhalf  9271  div4p1lem1div2  9290  difgtsumgt  9441  elz2  9443  zindd  9490  qapne  9759  divge1  9844  xrlttri3  9918  fseq1p1m1  10215  fzrevral  10226  nn0disj  10259  fzo0addel  10315  fzosplitsnm1  10336  fzosplitprm1  10361  flqlelt  10417  divfl0  10437  flqpmodeq  10470  zmodidfzo  10496  modqmuladd  10509  qnegmod  10512  addmodid  10515  modifeq2int  10529  modqeqmodmin  10537  modfzo0difsn  10538  modsumfzodifsn  10539  addmodlteq  10541  frecuzrdgsuc  10557  frecfzen2  10570  iseqf1olemab  10645  iseqf1olemmo  10648  seqf1oglem1  10662  seqf1oglem2  10663  ser3sub  10666  expgt1  10720  leexp2r  10736  sqoddm1div8  10836  mulsubdivbinom2ap  10854  bcm1k  10903  bcn2m1  10912  hashinfuni  10920  hashennnuni  10922  hashennn  10923  hashunlem  10947  hashprg  10951  fihashssdif  10961  zfz1isolem1  10983  elovmpowrd  11033  ccatsymb  11056  ccatlid  11060  eqs1  11080  shftlem  11098  shftfvalg  11100  shftfval  11103  replim  11141  cjexp  11175  resqrexlemcalc1  11296  resqrexlemcvg  11301  rersqrtthlem  11312  abssq  11363  recan  11391  negfi  11510  minclpr  11519  mingeb  11524  xrmaxiflemcom  11531  xrmineqinf  11551  xrminltinf  11554  xrminadd  11557  climmpt  11582  climrecl  11606  fsum3cvg  11660  summodclem3  11662  summodclem2a  11663  modfsummodlemstep  11739  isumsplit  11773  arisum  11780  geosergap  11788  geo2sum  11796  mertenslemi1  11817  mertenslem2  11818  clim2divap  11822  fproddccvg  11854  fprodssdc  11872  fprodabs  11898  fproddivapf  11913  fprodmodd  11923  efcj  11955  efsub  11963  eflegeo  11983  sinneg  12008  cosneg  12009  sin01bnd  12039  cos01bnd  12040  modm1div  12082  summodnegmod  12104  dvdseq  12130  addmodlteqALT  12141  mulmoddvds  12145  zob  12173  nn0ob  12190  divalgmod  12209  flodddiv4  12218  bitsinv1  12244  divgcdnnr  12268  gcdneg  12274  bezoutlemsup  12301  dvdssq  12323  lcmneg  12367  3lcm2e6woprm  12379  6lcm4e12  12380  divgcdcoprmex  12395  cncongr1  12396  cncongrcoprm  12399  oddpwdclemxy  12462  oddpwdclemodd  12465  divnumden  12489  zgcdsq  12494  phibnd  12510  hashgcdlem  12531  vfermltl  12545  powm2modprm  12546  reumodprminv  12547  pythagtriplem19  12576  pcprendvds2  12585  pczpre  12591  dvdsprmpweqle  12631  difsqpwdvds  12632  4sqlem4  12686  ennnfonelemex  12756  strndxid  12831  topnvalg  13054  prdssca  13078  intopsn  13170  ismgmid2  13183  mgmidsssn0  13187  gsumfzval  13194  gsumprval  13202  mndpfo  13241  mndfo  13242  mndinvmod  13248  prds0g  13252  mnd1id  13259  mhmf1o  13273  0mhm  13289  gsumwmhm  13301  grpidd2  13344  grpinvid2  13356  grpidssd  13379  grpnpcan  13395  grpsubsub4  13396  qusgrp2  13420  mulginvcom  13454  grpissubg  13501  quselbasg  13537  qus0  13542  ecqusaddd  13545  ghmid  13556  ghminv  13557  imasabl  13643  gsumfzmhm  13650  mgpress  13664  rnglz  13678  rngrz  13679  rngmneg1  13680  rngmneg2  13681  rngpropd  13688  srg1zr  13720  srgmulgass  13722  srgpcomp  13723  srgpcomppsc  13725  ringadd2  13760  ringo2times  13761  ringlz  13776  ringrz  13777  ringinvnzdiv  13783  ringnegl  13784  ringnegr  13785  imasring  13797  qusring2  13799  crngunit  13844  rhmopp  13909  lringuplu  13929  opprdomnbg  14007  lmod0vs  14054  lmodvsmmulgdi  14056  lmodfopne  14059  islss3  14112  lspsn  14149  lmodindp1  14161  rnglidlmmgm  14229  rnglidlmsgrp  14230  rnglidlrng  14231  isridl  14237  zringinvg  14337  zndvds  14382  znf1o  14384  psrgrp  14418  toponcom  14470  tgtopon  14509  restopnb  14624  cnptoprest  14682  blfvalps  14828  bdmopn  14947  cnmet  14973  mpomulcn  15009  limcdifap  15105  dvidsslem  15136  dviaddf  15148  dvexp  15154  dvply2g  15209  coseq0negpitopi  15279  abssinper  15289  rplogbzexp  15397  dvdsppwf1o  15432  mpodvdsmulf1o  15433  fsumdvdsmul  15434  sgmmul  15439  perfect  15444  lgsvalmod  15467  lgsneg  15472  gausslemma2dlem1a  15506  gausslemma2dlem6  15515  gausslemma2dlem7  15516  gausslemma2d  15517  lgsquadlem2  15526  2lgslem1a1  15534  2lgslem1a  15536  2lgslem3c  15543  2lgslem3d  15544  2lgslem3d1  15548  2lgs  15552  2lgsoddprm  15561  subctctexmid  15899  cvgcmp2nlemabs  15933  trilpolemlt1  15942