Theorem eqcomd 2237

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 2233	. 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 2213

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

This theorem is referenced by:  eqtr2d  2265  eqtr3d  2266  eqtr4d  2267  eqtr2id  2277  eqtr2di  2281  sylan9req  2285  eqeltrrd  2309  eleqtrrd  2311  eleqtrrid  2321  eqeltrrdi  2323  eqnetrrd  2429  neeqtrrd  2433  rspcedeq2vd  2921  dedhb  2976  eqsstrrd  3265  sseqtrrd  3267  eqsstrrdi  3281  dfrab3ss  3487  uneqdifeqim  3582  ifbothdadc  3643  ifbothdc  3644  2if2dc  3649  disjsn2  3736  diftpsn3  3819  elpr2elpr  3864  dfopg  3865  unimax  3932  sndisj  4089  eqbrtrrd  4117  breqtrrd  4121  breqtrrid  4131  eqbrtrrdi  4133  class2seteq  4259  opth1  4334  euotd  4353  opelopabsb  4360  tfisi  4691  0nelxp  4759  opeliunxp  4787  euiotaex  5310  iota4  5313  iotam  5325  fun2ssres  5377  funimass1  5414  funssfv  5674  fnimapr  5715  fvun1  5721  fvco4  5727  elfvmptrab  5751  fmptco  5821  fncofn  5840  foima2  5902  foeqcnvco  5941  f1eqcocnv  5942  f1oiso2  5978  riotass2  6010  riotass  6011  f1ocnvfv3  6017  fvmpopr2d  6168  caovlem2d  6225  f1opw2  6239  offveq  6265  sbcopeq1a  6359  csbopeq1a  6360  eloprabi  6370  cnvf1olem  6398  f2ndf  6400  suppval1  6417  suppsnopdc  6428  smoiso  6511  nnaword  6722  eqer  6777  uniqs  6805  mapsncnv  6907  ixpiinm  6936  mapsnf1o  6949  ssenen  7080  findcard2  7121  findcard2s  7122  unsnfidcex  7155  fisseneq  7170  phpeqd  7171  en1eqsn  7190  sbthlemi6  7204  updjud  7324  omp1eomlem  7336  nnnninf2  7369  nninfisollem0  7372  nninfisollemeq  7374  fodju0  7389  3nsssucpw1  7497  enq0sym  7695  enq0tr  7697  recexgt0sr  8036  caucvgsrlemoffcau  8061  axcaucvglemval  8160  le2tri3i  8330  cnegexlem2  8397  nnpcan  8444  addlsub  8591  negf1o  8603  subdi  8606  rereim  8808  cru  8824  divmulassap  8917  divmulasscomap  8918  divap1d  9023  subhalfhalf  9421  div4p1lem1div2  9440  difgtsumgt  9593  elz2  9595  zindd  9642  qapne  9917  divge1  10002  xrlttri3  10076  fseq1p1m1  10374  fzrevral  10385  nn0disj  10418  fzo0addel  10479  fzosplitsnm1  10500  fzosplitprm1  10526  flqlelt  10582  divfl0  10602  flqpmodeq  10635  zmodidfzo  10661  modqmuladd  10674  qnegmod  10677  addmodid  10680  modifeq2int  10694  modqeqmodmin  10702  modfzo0difsn  10703  modsumfzodifsn  10704  addmodlteq  10706  frecuzrdgsuc  10722  frecfzen2  10735  iseqf1olemab  10810  iseqf1olemmo  10813  seqf1oglem1  10827  seqf1oglem2  10828  ser3sub  10831  expgt1  10885  leexp2r  10901  sqoddm1div8  11001  mulsubdivbinom2ap  11019  bcm1k  11068  bcn2m1  11077  hashinfuni  11085  hashennnuni  11087  hashennn  11088  hashunlem  11113  hashprg  11118  fihashssdif  11128  zfz1isolem1  11150  elovmpowrd  11204  ccatsymb  11228  ccatlid  11232  eqs1  11254  ccatw2s1p1g  11271  swrdfv2  11293  swrds1  11298  swrdlsw  11299  pfxfv  11314  swrdswrd  11335  swrdpfx  11337  pfxpfx  11338  pfxlswccat  11343  ccats1pfxeq  11344  wrdind  11352  wrd2ind  11353  pfxccatin12lem1  11358  pfxccatin12lem2  11361  swrdccat3blem  11369  swrdccat3b  11370  ccats1pfxeqbi  11372  reuccatpfxs1lem  11376  reuccatpfxs1  11377  s3s4d  11433  s2s5d  11434  s5s2d  11435  shftlem  11439  shftfvalg  11441  shftfval  11444  replim  11482  cjexp  11516  resqrexlemcalc1  11637  resqrexlemcvg  11642  rersqrtthlem  11653  abssq  11704  recan  11732  negfi  11851  minclpr  11860  mingeb  11865  xrmaxiflemcom  11872  xrmineqinf  11892  xrminltinf  11895  xrminadd  11898  climmpt  11923  climrecl  11947  fsum3cvg  12002  summodclem3  12004  summodclem2a  12005  modfsummodlemstep  12081  isumsplit  12115  arisum  12122  geosergap  12130  geo2sum  12138  mertenslemi1  12159  mertenslem2  12160  clim2divap  12164  fproddccvg  12196  fprodssdc  12214  fprodabs  12240  fproddivapf  12255  fprodmodd  12265  efcj  12297  efsub  12305  eflegeo  12325  sinneg  12350  cosneg  12351  sin01bnd  12381  cos01bnd  12382  modm1div  12424  summodnegmod  12446  dvdseq  12472  addmodlteqALT  12483  mulmoddvds  12487  zob  12515  nn0ob  12532  divalgmod  12551  flodddiv4  12560  bitsinv1  12586  divgcdnnr  12610  gcdneg  12616  bezoutlemsup  12643  dvdssq  12665  lcmneg  12709  3lcm2e6woprm  12721  6lcm4e12  12722  divgcdcoprmex  12737  cncongr1  12738  cncongrcoprm  12741  oddpwdclemxy  12804  oddpwdclemodd  12807  divnumden  12831  zgcdsq  12836  phibnd  12852  hashgcdlem  12873  vfermltl  12887  powm2modprm  12888  reumodprminv  12889  pythagtriplem19  12918  pcprendvds2  12927  pczpre  12933  dvdsprmpweqle  12973  difsqpwdvds  12974  4sqlem4  13028  ennnfonelemex  13098  strndxid  13173  topnvalg  13397  prdssca  13421  intopsn  13513  ismgmid2  13526  mgmidsssn0  13530  gsumfzval  13537  gsumprval  13545  mndpfo  13584  mndfo  13585  mndinvmod  13591  prds0g  13595  mnd1id  13602  mhmf1o  13616  0mhm  13632  gsumwmhm  13644  grpidd2  13687  grpinvid2  13699  grpidssd  13722  grpnpcan  13738  grpsubsub4  13739  qusgrp2  13763  mulginvcom  13797  grpissubg  13844  quselbasg  13880  qus0  13885  ecqusaddd  13888  ghmid  13899  ghminv  13900  imasabl  13986  gsumfzmhm  13993  gsumsplit0  13996  mgpress  14008  rnglz  14022  rngrz  14023  rngmneg1  14024  rngmneg2  14025  rngpropd  14032  srg1zr  14064  srgmulgass  14066  srgpcomp  14067  srgpcomppsc  14069  ringadd2  14104  ringo2times  14105  ringlz  14120  ringrz  14121  ringinvnzdiv  14127  ringnegl  14128  ringnegr  14129  imasring  14141  qusring2  14143  crngunit  14189  rhmopp  14254  lringuplu  14274  opprdomnbg  14353  lmod0vs  14400  lmodvsmmulgdi  14402  lmodfopne  14405  islss3  14458  lspsn  14495  lmodindp1  14507  rnglidlmmgm  14575  rnglidlmsgrp  14576  rnglidlrng  14577  isridl  14583  zringinvg  14683  zndvds  14728  znf1o  14730  psrgrp  14769  toponcom  14821  tgtopon  14860  restopnb  14975  cnptoprest  15033  blfvalps  15179  bdmopn  15298  cnmet  15324  mpomulcn  15360  limcdifap  15456  dvidsslem  15487  dviaddf  15499  dvexp  15505  dvply2g  15560  coseq0negpitopi  15630  abssinper  15640  rplogbzexp  15748  pellexlem2  15775  dvdsppwf1o  15786  mpodvdsmulf1o  15787  fsumdvdsmul  15788  sgmmul  15793  perfect  15798  lgsvalmod  15821  lgsneg  15826  gausslemma2dlem1a  15860  gausslemma2dlem6  15869  gausslemma2dlem7  15870  gausslemma2d  15871  lgsquadlem2  15880  2lgslem1a1  15888  2lgslem1a  15890  2lgslem3c  15897  2lgslem3d  15898  2lgslem3d1  15902  2lgs  15906  2lgsoddprm  15915  uhgrun  16010  upgrun  16050  umgrun  16052  ushgredgedg  16150  issubgr2  16182  uhgrissubgr  16185  subgruhgredgdm  16194  subumgredg2en  16195  subupgr  16197  p1evtxdeqfilem  16235  wlklenvm1  16265  wlklenvm1g  16266  wlkl1loop  16282  upgriswlkdc  16284  uspgr2wlkeq  16289  uspgr2wlkeq2  16290  uspgr2wlkeqi  16291  wlkres  16303  loopclwwlkn1b  16343  clwwlkn1loopb  16344  clwwlkext2edg  16346  clwwlknonccat  16357  s2elclwwlknon2  16360  clwwlknonex2lem2  16362  clwwlknun  16365  eupth2lem3fi  16400  eupth2lembfi  16401  subctctexmid  16705  cvgcmp2nlemabs  16747  trilpolemlt1  16756  gsumgfsumlem  16795  gfsumsn  16797