Theorem eqcomd 2240

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 2236	. 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 2216

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

This theorem is referenced by:  eqtr2d  2268  eqtr3d  2269  eqtr4d  2270  eqtr2id  2280  eqtr2di  2284  sylan9req  2288  eqeltrrd  2312  eleqtrrd  2314  eleqtrrid  2324  eqeltrrdi  2326  eqabcdv  2366  eqnetrrd  2440  neeqtrrd  2444  rspcedeq2vd  2934  dedhb  2989  eqsstrrd  3279  sseqtrrd  3281  eqsstrrdi  3295  dfrab3ss  3503  uneqdifeqim  3599  ifbothdadc  3660  ifbothdc  3661  2if2dc  3666  ifeqeqxdc  3673  disjsn2  3757  diftpsn3  3840  elpr2elpr  3885  dfopg  3886  unimax  3953  sndisj  4110  eqbrtrrd  4138  breqtrrd  4142  breqtrrid  4152  eqbrtrrdi  4154  class2seteq  4281  opth1  4357  euotd  4376  opelopabsb  4383  tfisi  4714  0nelxp  4782  opeliunxp  4810  euiotaex  5334  iota4  5337  iotam  5349  fun2ssres  5401  funimass1  5438  funssfv  5701  fnimapr  5742  fvun1  5748  fvco4  5754  elfvmptrab  5778  fmptco  5848  fncofn  5867  foima2  5930  foeqcnvco  5969  f1eqcocnv  5970  f1oiso2  6006  riotass2  6040  riotass  6041  f1ocnvfv3  6047  fvmpopr2d  6198  caovlem2d  6255  f1opw2  6269  offveq  6296  sbcopeq1a  6394  csbopeq1a  6395  eloprabi  6405  cnvf1olem  6433  f2ndf  6435  suppval1  6452  suppsnopdc  6463  smoiso  6546  nnaword  6757  eqer  6812  uniqs  6840  mapsncnv  6943  ixpiinm  6972  mapsnf1o  6985  mapunen  7117  ssenen  7118  findcard2  7159  findcard2s  7160  unsnfidcex  7193  fisseneq  7208  phpeqd  7209  en1eqsn  7231  sbthlemi6  7245  updjud  7386  omp1eomlem  7398  nnnninf2  7431  nninfisollem0  7434  nninfisollemeq  7436  fodju0  7451  3nsssucpw1  7559  enq0sym  7763  enq0tr  7765  recexgt0sr  8104  caucvgsrlemoffcau  8129  axcaucvglemval  8228  le2tri3i  8398  cnegexlem2  8465  nnpcan  8512  addlsub  8659  negf1o  8672  subdi  8675  rereim  8877  cru  8893  divmulassap  8986  divmulasscomap  8987  divap1d  9092  subhalfhalf  9490  div4p1lem1div2  9509  difgtsumgt  9664  elz2  9666  zindd  9714  qapne  9989  divge1  10074  xrlttri3  10149  fseq1p1m1  10450  fzrevral  10461  nn0disj  10494  fzo0addel  10555  fzosplitsnm1  10576  fzosplitprm1  10602  flqlelt  10660  divfl0  10680  flqpmodeq  10713  zmodidfzo  10739  modqmuladd  10752  qnegmod  10755  addmodid  10758  modifeq2int  10772  modqeqmodmin  10780  modfzo0difsn  10781  modsumfzodifsn  10782  addmodlteq  10784  frecuzrdgsuc  10800  frecfzen2  10813  iseqf1olemab  10888  iseqf1olemmo  10891  seqf1oglem1  10905  seqf1oglem2  10906  ser3sub  10909  expgt1  10963  leexp2r  10979  sqoddm1div8  11080  mulsubdivbinom2ap  11098  bcm1k  11147  bcn2m1  11157  hashinfuni  11165  hashennnuni  11167  hashennn  11168  hashunlem  11193  hashprg  11198  fihashssdif  11208  hashfibclem  11231  hashfibc  11232  zfz1isolem1  11237  elovmpowrd  11291  ccatsymb  11315  ccatlid  11319  eqs1  11341  ccatw2s1p1g  11358  swrdfv2  11380  swrds1  11385  swrdlsw  11386  pfxfv  11401  swrdswrd  11422  swrdpfx  11424  pfxpfx  11425  pfxlswccat  11430  ccats1pfxeq  11431  wrdind  11439  wrd2ind  11440  pfxccatin12lem1  11445  pfxccatin12lem2  11448  swrdccat3blem  11456  swrdccat3b  11457  ccats1pfxeqbi  11459  reuccatpfxs1lem  11463  reuccatpfxs1  11464  s3s4d  11520  s2s5d  11521  s5s2d  11522  shftlem  11526  shftfvalg  11528  shftfval  11531  replim  11569  cjexp  11603  resqrexlemcalc1  11724  resqrexlemcvg  11729  rersqrtthlem  11740  abssq  11791  recan  11819  negfi  11938  minclpr  11947  mingeb  11952  xrmaxiflemcom  11959  xrmineqinf  11979  xrminltinf  11982  xrminadd  11985  climmpt  12010  climrecl  12034  fsum3cvg  12089  summodclem3  12091  summodclem2a  12092  modfsummodlemstep  12168  isumsplit  12202  arisum  12209  geosergap  12217  geo2sum  12225  mertenslemi1  12246  mertenslem2  12247  clim2divap  12251  fproddccvg  12283  fprodssdc  12301  fprodabs  12327  fproddivapf  12342  fprodmodd  12352  efcj  12384  efsub  12392  eflegeo  12412  sinneg  12437  cosneg  12438  sin01bnd  12468  cos01bnd  12469  modm1div  12511  summodnegmod  12533  dvdseq  12559  addmodlteqALT  12570  mulmoddvds  12574  zob  12602  nn0ob  12619  divalgmod  12638  flodddiv4  12647  bitsinv1  12673  divgcdnnr  12697  gcdneg  12703  bezoutlemsup  12730  dvdssq  12752  lcmneg  12796  3lcm2e6woprm  12808  6lcm4e12  12809  divgcdcoprmex  12824  cncongr1  12825  cncongrcoprm  12828  oddpwdclemxy  12891  oddpwdclemodd  12894  divnumden  12918  zgcdsq  12923  phibnd  12939  hashgcdlem  12960  vfermltl  12974  powm2modprm  12975  reumodprminv  12976  pythagtriplem19  13005  pcprendvds2  13014  pczpre  13020  dvdsprmpweqle  13060  difsqpwdvds  13061  4sqlem4  13115  ballotfilemfp1  13175  ballotfilemsf1o  13201  ballotfilemrinv0  13220  ennnfonelemex  13249  strndxid  13324  topnvalg  13548  intopsn  13630  ismgmid2  13643  mgmidsssn0  13647  gsumfzval  13654  gsumprval  13662  mndpfo  13699  mndfo  13700  mndinvmod  13706  mnd1id  13711  mhmf1o  13725  0mhm  13741  gsumwmhm  13753  grpidd2  13796  grpinvid2  13808  grpidssd  13831  grpnpcan  13847  grpsubsub4  13848  qusgrp2  13866  mulginvcom  13900  grpissubg  13947  quselbasg  13983  qus0  13988  ecqusaddd  13991  ghmid  14002  ghminv  14003  imasabl  14089  gsumfzmhm  14096  gsumsplit0  14099  gsumshift  14105  gfsumsn  14107  prdssca  14117  prds0g  14137  mgpress  14170  rnglz  14184  rngrz  14185  rngmneg1  14186  rngmneg2  14187  rngpropd  14194  rng1zrlem  14198  srgmulgass  14232  srgpcomp  14233  srgpcomppsc  14235  ringadd2  14270  ringo2times  14271  ringlz  14286  ringrz  14287  ringinvnzdiv  14293  ringnegl  14294  ringnegr  14295  imasring  14307  qusring2  14309  crngunit  14356  rhmopp  14421  lringuplu  14441  opprdomnbg  14521  lmod0vs  14595  lmodvsmmulgdi  14597  lmodfopne  14600  islss3  14653  lspsn  14690  lmodindp1  14702  rnglidlmmgm  14770  rnglidlmsgrp  14771  rnglidlrng  14772  isridl  14778  zringinvg  14878  zndvds  14923  znf1o  14925  psrgrp  14966  toponcom  15018  tgtopon  15057  restopnb  15172  cnptoprest  15230  blfvalps  15376  bdmopn  15495  cnmet  15521  mpomulcn  15557  limcdifap  15653  dvidsslem  15684  dviaddf  15696  dvexp  15702  dvply2g  15757  coseq0negpitopi  15827  abssinper  15837  rplogbzexp  15945  pellexlem2  15972  dvdsppwf1o  15983  mpodvdsmulf1o  15984  fsumdvdsmul  15985  sgmmul  15990  perfect  15995  lgsvalmod  16018  lgsneg  16023  gausslemma2dlem1a  16057  gausslemma2dlem6  16066  gausslemma2dlem7  16067  gausslemma2d  16068  lgsquadlem2  16077  2lgslem1a1  16085  2lgslem1a  16087  2lgslem3c  16094  2lgslem3d  16095  2lgslem3d1  16099  2lgs  16103  2lgsoddprm  16112  uhgrun  16207  upgrun  16247  umgrun  16249  ushgredgedg  16347  issubgr2  16379  uhgrissubgr  16382  subgruhgredgdm  16391  subumgredg2en  16392  subupgr  16394  p1evtxdeqfilem  16432  wlklenvm1  16462  wlklenvm1g  16463  wlkl1loop  16479  upgriswlkdc  16481  uspgr2wlkeq  16486  uspgr2wlkeq2  16487  uspgr2wlkeqi  16488  wlkres  16500  loopclwwlkn1b  16540  clwwlkn1loopb  16541  clwwlkext2edg  16543  clwwlknonccat  16554  s2elclwwlknon2  16557  clwwlknonex2lem2  16559  clwwlknun  16562  eupth2lem3fi  16597  eupth2lembfi  16598  subctctexmid  16900  cvgcmp2nlemabs  16942  trilpolemlt1  16951