Theorem eqcomd 2202

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-ext 2178

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

This theorem is referenced by:  eqtr2d  2230  eqtr3d  2231  eqtr4d  2232  eqtr2id  2242  eqtr2di  2246  sylan9req  2250  eqeltrrd  2274  eleqtrrd  2276  eleqtrrid  2286  eqeltrrdi  2288  eqnetrrd  2393  neeqtrrd  2397  rspcedeq2vd  2878  dedhb  2933  eqsstrrd  3220  sseqtrrd  3222  eqsstrrdi  3236  dfrab3ss  3441  uneqdifeqim  3536  ifbothdadc  3593  ifbothdc  3594  disjsn2  3685  diftpsn3  3763  dfopg  3806  unimax  3873  sndisj  4029  eqbrtrrd  4057  breqtrrd  4061  breqtrrid  4071  eqbrtrrdi  4073  class2seteq  4196  opth1  4269  euotd  4287  opelopabsb  4294  tfisi  4623  0nelxp  4691  opeliunxp  4718  euiotaex  5235  iota4  5238  iotam  5250  fun2ssres  5301  funimass1  5335  funssfv  5584  fnimapr  5621  fvun1  5627  fvco4  5633  elfvmptrab  5657  fmptco  5728  foima2  5798  foeqcnvco  5837  f1eqcocnv  5838  f1oiso2  5874  riotass2  5904  riotass  5905  f1ocnvfv3  5911  fvmpopr2d  6059  caovlem2d  6116  f1opw2  6129  sbcopeq1a  6245  csbopeq1a  6246  eloprabi  6254  cnvf1olem  6282  f2ndf  6284  smoiso  6360  nnaword  6569  eqer  6624  uniqs  6652  mapsncnv  6754  ixpiinm  6783  mapsnf1o  6796  ssenen  6912  findcard2  6950  findcard2s  6951  unsnfidcex  6981  fisseneq  6995  phpeqd  6996  en1eqsn  7014  sbthlemi6  7028  updjud  7148  omp1eomlem  7160  nnnninf2  7193  nninfisollem0  7196  nninfisollemeq  7198  fodju0  7213  3nsssucpw1  7303  enq0sym  7499  enq0tr  7501  recexgt0sr  7840  caucvgsrlemoffcau  7865  axcaucvglemval  7964  le2tri3i  8135  cnegexlem2  8202  nnpcan  8249  addlsub  8396  negf1o  8408  subdi  8411  rereim  8613  cru  8629  divmulassap  8722  divmulasscomap  8723  divap1d  8828  subhalfhalf  9226  div4p1lem1div2  9245  difgtsumgt  9395  elz2  9397  zindd  9444  qapne  9713  divge1  9798  xrlttri3  9872  fseq1p1m1  10169  fzrevral  10180  nn0disj  10213  fzosplitsnm1  10285  fzosplitprm1  10310  flqlelt  10366  divfl0  10386  flqpmodeq  10419  zmodidfzo  10445  modqmuladd  10458  qnegmod  10461  addmodid  10464  modifeq2int  10478  modqeqmodmin  10486  modfzo0difsn  10487  modsumfzodifsn  10488  addmodlteq  10490  frecuzrdgsuc  10506  frecfzen2  10519  iseqf1olemab  10594  iseqf1olemmo  10597  seqf1oglem1  10611  seqf1oglem2  10612  ser3sub  10615  expgt1  10669  leexp2r  10685  sqoddm1div8  10785  mulsubdivbinom2ap  10803  bcm1k  10852  bcn2m1  10861  hashinfuni  10869  hashennnuni  10871  hashennn  10872  hashunlem  10896  hashprg  10900  fihashssdif  10910  zfz1isolem1  10932  elovmpowrd  10976  shftlem  10981  shftfvalg  10983  shftfval  10986  replim  11024  cjexp  11058  resqrexlemcalc1  11179  resqrexlemcvg  11184  rersqrtthlem  11195  abssq  11246  recan  11274  negfi  11393  minclpr  11402  mingeb  11407  xrmaxiflemcom  11414  xrmineqinf  11434  xrminltinf  11437  xrminadd  11440  climmpt  11465  climrecl  11489  fsum3cvg  11543  summodclem3  11545  summodclem2a  11546  modfsummodlemstep  11622  isumsplit  11656  arisum  11663  geosergap  11671  geo2sum  11679  mertenslemi1  11700  mertenslem2  11701  clim2divap  11705  fproddccvg  11737  fprodssdc  11755  fprodabs  11781  fproddivapf  11796  fprodmodd  11806  efcj  11838  efsub  11846  eflegeo  11866  sinneg  11891  cosneg  11892  sin01bnd  11922  cos01bnd  11923  modm1div  11965  summodnegmod  11987  dvdseq  12013  addmodlteqALT  12024  mulmoddvds  12028  zob  12056  nn0ob  12073  divalgmod  12092  flodddiv4  12101  divgcdnnr  12143  gcdneg  12149  bezoutlemsup  12176  dvdssq  12198  lcmneg  12242  3lcm2e6woprm  12254  6lcm4e12  12255  divgcdcoprmex  12270  cncongr1  12271  cncongrcoprm  12274  oddpwdclemxy  12337  oddpwdclemodd  12340  divnumden  12364  zgcdsq  12369  phibnd  12385  hashgcdlem  12406  vfermltl  12420  powm2modprm  12421  reumodprminv  12422  pythagtriplem19  12451  pcprendvds2  12460  pczpre  12466  dvdsprmpweqle  12506  difsqpwdvds  12507  4sqlem4  12561  ennnfonelemex  12631  strndxid  12706  topnvalg  12922  intopsn  13010  ismgmid2  13023  mgmidsssn0  13027  gsumfzval  13034  gsumprval  13042  mndpfo  13079  mndfo  13080  mndinvmod  13086  mnd1id  13088  mhmf1o  13102  0mhm  13118  gsumwmhm  13130  grpidd2  13173  grpinvid2  13185  grpidssd  13208  grpnpcan  13224  grpsubsub4  13225  qusgrp2  13243  mulginvcom  13277  grpissubg  13324  quselbasg  13360  qus0  13365  ecqusaddd  13368  ghmid  13379  ghminv  13380  imasabl  13466  gsumfzmhm  13473  mgpress  13487  rnglz  13501  rngrz  13502  rngmneg1  13503  rngmneg2  13504  rngpropd  13511  srg1zr  13543  srgmulgass  13545  srgpcomp  13546  srgpcomppsc  13548  ringadd2  13583  ringo2times  13584  ringlz  13599  ringrz  13600  ringinvnzdiv  13606  ringnegl  13607  ringnegr  13608  imasring  13620  qusring2  13622  crngunit  13667  rhmopp  13732  lringuplu  13752  opprdomnbg  13830  lmod0vs  13877  lmodvsmmulgdi  13879  lmodfopne  13882  islss3  13935  lspsn  13972  lmodindp1  13984  rnglidlmmgm  14052  rnglidlmsgrp  14053  rnglidlrng  14054  isridl  14060  zringinvg  14160  zndvds  14205  znf1o  14207  toponcom  14263  tgtopon  14302  restopnb  14417  cnptoprest  14475  blfvalps  14621  bdmopn  14740  cnmet  14766  mpomulcn  14802  limcdifap  14898  dvidsslem  14929  dviaddf  14941  dvexp  14947  dvply2g  15002  coseq0negpitopi  15072  abssinper  15082  rplogbzexp  15190  dvdsppwf1o  15225  mpodvdsmulf1o  15226  fsumdvdsmul  15227  sgmmul  15232  perfect  15237  lgsvalmod  15260  lgsneg  15265  gausslemma2dlem1a  15299  gausslemma2dlem6  15308  gausslemma2dlem7  15309  gausslemma2d  15310  lgsquadlem2  15319  2lgslem1a1  15327  2lgslem1a  15329  2lgslem3c  15336  2lgslem3d  15337  2lgslem3d1  15341  2lgs  15345  2lgsoddprm  15354  subctctexmid  15645  cvgcmp2nlemabs  15676  trilpolemlt1  15685