Theorem eqcomd 2238

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-ext 2214

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

This theorem is referenced by:  eqtr2d  2266  eqtr3d  2267  eqtr4d  2268  eqtr2id  2278  eqtr2di  2282  sylan9req  2286  eqeltrrd  2310  eleqtrrd  2312  eleqtrrid  2322  eqeltrrdi  2324  eqabcdv  2364  eqnetrrd  2438  neeqtrrd  2442  rspcedeq2vd  2931  dedhb  2986  eqsstrrd  3275  sseqtrrd  3277  eqsstrrdi  3291  dfrab3ss  3499  uneqdifeqim  3595  ifbothdadc  3656  ifbothdc  3657  2if2dc  3662  disjsn2  3752  diftpsn3  3835  elpr2elpr  3880  dfopg  3881  unimax  3948  sndisj  4105  eqbrtrrd  4133  breqtrrd  4137  breqtrrid  4147  eqbrtrrdi  4149  class2seteq  4276  opth1  4352  euotd  4371  opelopabsb  4378  tfisi  4709  0nelxp  4777  opeliunxp  4805  euiotaex  5329  iota4  5332  iotam  5344  fun2ssres  5396  funimass1  5433  funssfv  5696  fnimapr  5737  fvun1  5743  fvco4  5749  elfvmptrab  5773  fmptco  5843  fncofn  5862  foima2  5924  foeqcnvco  5963  f1eqcocnv  5964  f1oiso2  6000  riotass2  6032  riotass  6033  f1ocnvfv3  6039  fvmpopr2d  6190  caovlem2d  6247  f1opw2  6261  offveq  6287  sbcopeq1a  6381  csbopeq1a  6382  eloprabi  6392  cnvf1olem  6420  f2ndf  6422  suppval1  6439  suppsnopdc  6450  smoiso  6533  nnaword  6744  eqer  6799  uniqs  6827  mapsncnv  6930  ixpiinm  6959  mapsnf1o  6972  mapunen  7104  ssenen  7105  findcard2  7146  findcard2s  7147  unsnfidcex  7180  fisseneq  7195  phpeqd  7196  en1eqsn  7218  sbthlemi6  7232  updjud  7373  omp1eomlem  7385  nnnninf2  7418  nninfisollem0  7421  nninfisollemeq  7423  fodju0  7438  3nsssucpw1  7546  enq0sym  7747  enq0tr  7749  recexgt0sr  8088  caucvgsrlemoffcau  8113  axcaucvglemval  8212  le2tri3i  8382  cnegexlem2  8449  nnpcan  8496  addlsub  8643  negf1o  8655  subdi  8658  rereim  8860  cru  8876  divmulassap  8969  divmulasscomap  8970  divap1d  9075  subhalfhalf  9473  div4p1lem1div2  9492  difgtsumgt  9647  elz2  9649  zindd  9696  qapne  9971  divge1  10056  xrlttri3  10130  fseq1p1m1  10428  fzrevral  10439  nn0disj  10472  fzo0addel  10533  fzosplitsnm1  10554  fzosplitprm1  10580  flqlelt  10636  divfl0  10656  flqpmodeq  10689  zmodidfzo  10715  modqmuladd  10728  qnegmod  10731  addmodid  10734  modifeq2int  10748  modqeqmodmin  10756  modfzo0difsn  10757  modsumfzodifsn  10758  addmodlteq  10760  frecuzrdgsuc  10776  frecfzen2  10789  iseqf1olemab  10864  iseqf1olemmo  10867  seqf1oglem1  10881  seqf1oglem2  10882  ser3sub  10885  expgt1  10939  leexp2r  10955  sqoddm1div8  11055  mulsubdivbinom2ap  11073  bcm1k  11122  bcn2m1  11132  hashinfuni  11140  hashennnuni  11142  hashennn  11143  hashunlem  11168  hashprg  11173  fihashssdif  11183  hashfibclem  11206  hashfibc  11207  zfz1isolem1  11212  elovmpowrd  11266  ccatsymb  11290  ccatlid  11294  eqs1  11316  ccatw2s1p1g  11333  swrdfv2  11355  swrds1  11360  swrdlsw  11361  pfxfv  11376  swrdswrd  11397  swrdpfx  11399  pfxpfx  11400  pfxlswccat  11405  ccats1pfxeq  11406  wrdind  11414  wrd2ind  11415  pfxccatin12lem1  11420  pfxccatin12lem2  11423  swrdccat3blem  11431  swrdccat3b  11432  ccats1pfxeqbi  11434  reuccatpfxs1lem  11438  reuccatpfxs1  11439  s3s4d  11495  s2s5d  11496  s5s2d  11497  shftlem  11501  shftfvalg  11503  shftfval  11506  replim  11544  cjexp  11578  resqrexlemcalc1  11699  resqrexlemcvg  11704  rersqrtthlem  11715  abssq  11766  recan  11794  negfi  11913  minclpr  11922  mingeb  11927  xrmaxiflemcom  11934  xrmineqinf  11954  xrminltinf  11957  xrminadd  11960  climmpt  11985  climrecl  12009  fsum3cvg  12064  summodclem3  12066  summodclem2a  12067  modfsummodlemstep  12143  isumsplit  12177  arisum  12184  geosergap  12192  geo2sum  12200  mertenslemi1  12221  mertenslem2  12222  clim2divap  12226  fproddccvg  12258  fprodssdc  12276  fprodabs  12302  fproddivapf  12317  fprodmodd  12327  efcj  12359  efsub  12367  eflegeo  12387  sinneg  12412  cosneg  12413  sin01bnd  12443  cos01bnd  12444  modm1div  12486  summodnegmod  12508  dvdseq  12534  addmodlteqALT  12545  mulmoddvds  12549  zob  12577  nn0ob  12594  divalgmod  12613  flodddiv4  12622  bitsinv1  12648  divgcdnnr  12672  gcdneg  12678  bezoutlemsup  12705  dvdssq  12727  lcmneg  12771  3lcm2e6woprm  12783  6lcm4e12  12784  divgcdcoprmex  12799  cncongr1  12800  cncongrcoprm  12803  oddpwdclemxy  12866  oddpwdclemodd  12869  divnumden  12893  zgcdsq  12898  phibnd  12914  hashgcdlem  12935  vfermltl  12949  powm2modprm  12950  reumodprminv  12951  pythagtriplem19  12980  pcprendvds2  12989  pczpre  12995  dvdsprmpweqle  13035  difsqpwdvds  13036  4sqlem4  13090  ennnfonelemex  13165  strndxid  13240  topnvalg  13464  prdssca  13488  intopsn  13580  ismgmid2  13593  mgmidsssn0  13597  gsumfzval  13604  gsumprval  13612  mndpfo  13651  mndfo  13652  mndinvmod  13658  prds0g  13662  mnd1id  13669  mhmf1o  13683  0mhm  13699  gsumwmhm  13711  grpidd2  13754  grpinvid2  13766  grpidssd  13789  grpnpcan  13805  grpsubsub4  13806  qusgrp2  13830  mulginvcom  13864  grpissubg  13911  quselbasg  13947  qus0  13952  ecqusaddd  13955  ghmid  13966  ghminv  13967  imasabl  14053  gsumfzmhm  14060  gsumsplit0  14063  mgpress  14075  rnglz  14089  rngrz  14090  rngmneg1  14091  rngmneg2  14092  rngpropd  14099  srg1zr  14131  srgmulgass  14133  srgpcomp  14134  srgpcomppsc  14136  ringadd2  14171  ringo2times  14172  ringlz  14187  ringrz  14188  ringinvnzdiv  14194  ringnegl  14195  ringnegr  14196  imasring  14208  qusring2  14210  crngunit  14256  rhmopp  14321  lringuplu  14341  opprdomnbg  14420  lmod0vs  14469  lmodvsmmulgdi  14471  lmodfopne  14474  islss3  14527  lspsn  14564  lmodindp1  14576  rnglidlmmgm  14644  rnglidlmsgrp  14645  rnglidlrng  14646  isridl  14652  zringinvg  14752  zndvds  14797  znf1o  14799  psrgrp  14840  toponcom  14892  tgtopon  14931  restopnb  15046  cnptoprest  15104  blfvalps  15250  bdmopn  15369  cnmet  15395  mpomulcn  15431  limcdifap  15527  dvidsslem  15558  dviaddf  15570  dvexp  15576  dvply2g  15631  coseq0negpitopi  15701  abssinper  15711  rplogbzexp  15819  pellexlem2  15846  dvdsppwf1o  15857  mpodvdsmulf1o  15858  fsumdvdsmul  15859  sgmmul  15864  perfect  15869  lgsvalmod  15892  lgsneg  15897  gausslemma2dlem1a  15931  gausslemma2dlem6  15940  gausslemma2dlem7  15941  gausslemma2d  15942  lgsquadlem2  15951  2lgslem1a1  15959  2lgslem1a  15961  2lgslem3c  15968  2lgslem3d  15969  2lgslem3d1  15973  2lgs  15977  2lgsoddprm  15986  uhgrun  16081  upgrun  16121  umgrun  16123  ushgredgedg  16221  issubgr2  16253  uhgrissubgr  16256  subgruhgredgdm  16265  subumgredg2en  16266  subupgr  16268  p1evtxdeqfilem  16306  wlklenvm1  16336  wlklenvm1g  16337  wlkl1loop  16353  upgriswlkdc  16355  uspgr2wlkeq  16360  uspgr2wlkeq2  16361  uspgr2wlkeqi  16362  wlkres  16374  loopclwwlkn1b  16414  clwwlkn1loopb  16415  clwwlkext2edg  16417  clwwlknonccat  16428  s2elclwwlknon2  16431  clwwlknonex2lem2  16433  clwwlknun  16436  eupth2lem3fi  16471  eupth2lembfi  16472  subctctexmid  16774  cvgcmp2nlemabs  16816  trilpolemlt1  16825  gsumgfsumlem  16865  gfsumsn  16867