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  shftlem  11069  shftfvalg  11071  shftfval  11074  replim  11112  cjexp  11146  resqrexlemcalc1  11267  resqrexlemcvg  11272  rersqrtthlem  11283  abssq  11334  recan  11362  negfi  11481  minclpr  11490  mingeb  11495  xrmaxiflemcom  11502  xrmineqinf  11522  xrminltinf  11525  xrminadd  11528  climmpt  11553  climrecl  11577  fsum3cvg  11631  summodclem3  11633  summodclem2a  11634  modfsummodlemstep  11710  isumsplit  11744  arisum  11751  geosergap  11759  geo2sum  11767  mertenslemi1  11788  mertenslem2  11789  clim2divap  11793  fproddccvg  11825  fprodssdc  11843  fprodabs  11869  fproddivapf  11884  fprodmodd  11894  efcj  11926  efsub  11934  eflegeo  11954  sinneg  11979  cosneg  11980  sin01bnd  12010  cos01bnd  12011  modm1div  12053  summodnegmod  12075  dvdseq  12101  addmodlteqALT  12112  mulmoddvds  12116  zob  12144  nn0ob  12161  divalgmod  12180  flodddiv4  12189  bitsinv1  12215  divgcdnnr  12239  gcdneg  12245  bezoutlemsup  12272  dvdssq  12294  lcmneg  12338  3lcm2e6woprm  12350  6lcm4e12  12351  divgcdcoprmex  12366  cncongr1  12367  cncongrcoprm  12370  oddpwdclemxy  12433  oddpwdclemodd  12436  divnumden  12460  zgcdsq  12465  phibnd  12481  hashgcdlem  12502  vfermltl  12516  powm2modprm  12517  reumodprminv  12518  pythagtriplem19  12547  pcprendvds2  12556  pczpre  12562  dvdsprmpweqle  12602  difsqpwdvds  12603  4sqlem4  12657  ennnfonelemex  12727  strndxid  12802  topnvalg  13025  prdssca  13049  intopsn  13141  ismgmid2  13154  mgmidsssn0  13158  gsumfzval  13165  gsumprval  13173  mndpfo  13212  mndfo  13213  mndinvmod  13219  prds0g  13223  mnd1id  13230  mhmf1o  13244  0mhm  13260  gsumwmhm  13272  grpidd2  13315  grpinvid2  13327  grpidssd  13350  grpnpcan  13366  grpsubsub4  13367  qusgrp2  13391  mulginvcom  13425  grpissubg  13472  quselbasg  13508  qus0  13513  ecqusaddd  13516  ghmid  13527  ghminv  13528  imasabl  13614  gsumfzmhm  13621  mgpress  13635  rnglz  13649  rngrz  13650  rngmneg1  13651  rngmneg2  13652  rngpropd  13659  srg1zr  13691  srgmulgass  13693  srgpcomp  13694  srgpcomppsc  13696  ringadd2  13731  ringo2times  13732  ringlz  13747  ringrz  13748  ringinvnzdiv  13754  ringnegl  13755  ringnegr  13756  imasring  13768  qusring2  13770  crngunit  13815  rhmopp  13880  lringuplu  13900  opprdomnbg  13978  lmod0vs  14025  lmodvsmmulgdi  14027  lmodfopne  14030  islss3  14083  lspsn  14120  lmodindp1  14132  rnglidlmmgm  14200  rnglidlmsgrp  14201  rnglidlrng  14202  isridl  14208  zringinvg  14308  zndvds  14353  znf1o  14355  psrgrp  14389  toponcom  14441  tgtopon  14480  restopnb  14595  cnptoprest  14653  blfvalps  14799  bdmopn  14918  cnmet  14944  mpomulcn  14980  limcdifap  15076  dvidsslem  15107  dviaddf  15119  dvexp  15125  dvply2g  15180  coseq0negpitopi  15250  abssinper  15260  rplogbzexp  15368  dvdsppwf1o  15403  mpodvdsmulf1o  15404  fsumdvdsmul  15405  sgmmul  15410  perfect  15415  lgsvalmod  15438  lgsneg  15443  gausslemma2dlem1a  15477  gausslemma2dlem6  15486  gausslemma2dlem7  15487  gausslemma2d  15488  lgsquadlem2  15497  2lgslem1a1  15505  2lgslem1a  15507  2lgslem3c  15514  2lgslem3d  15515  2lgslem3d1  15519  2lgs  15523  2lgsoddprm  15532  subctctexmid  15870  cvgcmp2nlemabs  15904  trilpolemlt1  15913