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 1397

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 1495  ax-gen 1497  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  2428  neeqtrrd  2432  rspcedeq2vd  2920  dedhb  2975  eqsstrrd  3264  sseqtrrd  3266  eqsstrrdi  3280  dfrab3ss  3485  uneqdifeqim  3580  ifbothdadc  3639  ifbothdc  3640  2if2dc  3645  disjsn2  3732  diftpsn3  3814  elpr2elpr  3859  dfopg  3860  unimax  3927  sndisj  4084  eqbrtrrd  4112  breqtrrd  4116  breqtrrid  4126  eqbrtrrdi  4128  class2seteq  4253  opth1  4328  euotd  4347  opelopabsb  4354  tfisi  4685  0nelxp  4753  opeliunxp  4781  euiotaex  5303  iota4  5306  iotam  5318  fun2ssres  5370  funimass1  5407  funssfv  5665  fnimapr  5706  fvun1  5712  fvco4  5718  elfvmptrab  5742  fmptco  5813  fncofn  5832  foima2  5892  foeqcnvco  5931  f1eqcocnv  5932  f1oiso2  5968  riotass2  6000  riotass  6001  f1ocnvfv3  6007  fvmpopr2d  6158  caovlem2d  6215  f1opw2  6229  offveq  6256  sbcopeq1a  6350  csbopeq1a  6351  eloprabi  6361  cnvf1olem  6389  f2ndf  6391  smoiso  6468  nnaword  6679  eqer  6734  uniqs  6762  mapsncnv  6864  ixpiinm  6893  mapsnf1o  6906  ssenen  7037  findcard2  7078  findcard2s  7079  unsnfidcex  7112  fisseneq  7127  phpeqd  7128  en1eqsn  7147  sbthlemi6  7161  updjud  7281  omp1eomlem  7293  nnnninf2  7326  nninfisollem0  7329  nninfisollemeq  7331  fodju0  7346  3nsssucpw1  7454  enq0sym  7652  enq0tr  7654  recexgt0sr  7993  caucvgsrlemoffcau  8018  axcaucvglemval  8117  le2tri3i  8288  cnegexlem2  8355  nnpcan  8402  addlsub  8549  negf1o  8561  subdi  8564  rereim  8766  cru  8782  divmulassap  8875  divmulasscomap  8876  divap1d  8981  subhalfhalf  9379  div4p1lem1div2  9398  difgtsumgt  9549  elz2  9551  zindd  9598  qapne  9873  divge1  9958  xrlttri3  10032  fseq1p1m1  10329  fzrevral  10340  nn0disj  10373  fzo0addel  10434  fzosplitsnm1  10455  fzosplitprm1  10481  flqlelt  10537  divfl0  10557  flqpmodeq  10590  zmodidfzo  10616  modqmuladd  10629  qnegmod  10632  addmodid  10635  modifeq2int  10649  modqeqmodmin  10657  modfzo0difsn  10658  modsumfzodifsn  10659  addmodlteq  10661  frecuzrdgsuc  10677  frecfzen2  10690  iseqf1olemab  10765  iseqf1olemmo  10768  seqf1oglem1  10782  seqf1oglem2  10783  ser3sub  10786  expgt1  10840  leexp2r  10856  sqoddm1div8  10956  mulsubdivbinom2ap  10974  bcm1k  11023  bcn2m1  11032  hashinfuni  11040  hashennnuni  11042  hashennn  11043  hashunlem  11068  hashprg  11073  fihashssdif  11083  zfz1isolem1  11105  elovmpowrd  11159  ccatsymb  11183  ccatlid  11187  eqs1  11209  ccatw2s1p1g  11226  swrdfv2  11248  swrds1  11253  swrdlsw  11254  pfxfv  11269  swrdswrd  11290  swrdpfx  11292  pfxpfx  11293  pfxlswccat  11298  ccats1pfxeq  11299  wrdind  11307  wrd2ind  11308  pfxccatin12lem1  11313  pfxccatin12lem2  11316  swrdccat3blem  11324  swrdccat3b  11325  ccats1pfxeqbi  11327  reuccatpfxs1lem  11331  reuccatpfxs1  11332  s3s4d  11388  s2s5d  11389  s5s2d  11390  shftlem  11394  shftfvalg  11396  shftfval  11399  replim  11437  cjexp  11471  resqrexlemcalc1  11592  resqrexlemcvg  11597  rersqrtthlem  11608  abssq  11659  recan  11687  negfi  11806  minclpr  11815  mingeb  11820  xrmaxiflemcom  11827  xrmineqinf  11847  xrminltinf  11850  xrminadd  11853  climmpt  11878  climrecl  11902  fsum3cvg  11957  summodclem3  11959  summodclem2a  11960  modfsummodlemstep  12036  isumsplit  12070  arisum  12077  geosergap  12085  geo2sum  12093  mertenslemi1  12114  mertenslem2  12115  clim2divap  12119  fproddccvg  12151  fprodssdc  12169  fprodabs  12195  fproddivapf  12210  fprodmodd  12220  efcj  12252  efsub  12260  eflegeo  12280  sinneg  12305  cosneg  12306  sin01bnd  12336  cos01bnd  12337  modm1div  12379  summodnegmod  12401  dvdseq  12427  addmodlteqALT  12438  mulmoddvds  12442  zob  12470  nn0ob  12487  divalgmod  12506  flodddiv4  12515  bitsinv1  12541  divgcdnnr  12565  gcdneg  12571  bezoutlemsup  12598  dvdssq  12620  lcmneg  12664  3lcm2e6woprm  12676  6lcm4e12  12677  divgcdcoprmex  12692  cncongr1  12693  cncongrcoprm  12696  oddpwdclemxy  12759  oddpwdclemodd  12762  divnumden  12786  zgcdsq  12791  phibnd  12807  hashgcdlem  12828  vfermltl  12842  powm2modprm  12843  reumodprminv  12844  pythagtriplem19  12873  pcprendvds2  12882  pczpre  12888  dvdsprmpweqle  12928  difsqpwdvds  12929  4sqlem4  12983  ennnfonelemex  13053  strndxid  13128  topnvalg  13352  prdssca  13376  intopsn  13468  ismgmid2  13481  mgmidsssn0  13485  gsumfzval  13492  gsumprval  13500  mndpfo  13539  mndfo  13540  mndinvmod  13546  prds0g  13550  mnd1id  13557  mhmf1o  13571  0mhm  13587  gsumwmhm  13599  grpidd2  13642  grpinvid2  13654  grpidssd  13677  grpnpcan  13693  grpsubsub4  13694  qusgrp2  13718  mulginvcom  13752  grpissubg  13799  quselbasg  13835  qus0  13840  ecqusaddd  13843  ghmid  13854  ghminv  13855  imasabl  13941  gsumfzmhm  13948  gsumsplit0  13951  mgpress  13963  rnglz  13977  rngrz  13978  rngmneg1  13979  rngmneg2  13980  rngpropd  13987  srg1zr  14019  srgmulgass  14021  srgpcomp  14022  srgpcomppsc  14024  ringadd2  14059  ringo2times  14060  ringlz  14075  ringrz  14076  ringinvnzdiv  14082  ringnegl  14083  ringnegr  14084  imasring  14096  qusring2  14098  crngunit  14144  rhmopp  14209  lringuplu  14229  opprdomnbg  14307  lmod0vs  14354  lmodvsmmulgdi  14356  lmodfopne  14359  islss3  14412  lspsn  14449  lmodindp1  14461  rnglidlmmgm  14529  rnglidlmsgrp  14530  rnglidlrng  14531  isridl  14537  zringinvg  14637  zndvds  14682  znf1o  14684  psrgrp  14718  toponcom  14770  tgtopon  14809  restopnb  14924  cnptoprest  14982  blfvalps  15128  bdmopn  15247  cnmet  15273  mpomulcn  15309  limcdifap  15405  dvidsslem  15436  dviaddf  15448  dvexp  15454  dvply2g  15509  coseq0negpitopi  15579  abssinper  15589  rplogbzexp  15697  dvdsppwf1o  15732  mpodvdsmulf1o  15733  fsumdvdsmul  15734  sgmmul  15739  perfect  15744  lgsvalmod  15767  lgsneg  15772  gausslemma2dlem1a  15806  gausslemma2dlem6  15815  gausslemma2dlem7  15816  gausslemma2d  15817  lgsquadlem2  15826  2lgslem1a1  15834  2lgslem1a  15836  2lgslem3c  15843  2lgslem3d  15844  2lgslem3d1  15848  2lgs  15852  2lgsoddprm  15861  uhgrun  15956  upgrun  15996  umgrun  15998  ushgredgedg  16096  issubgr2  16128  uhgrissubgr  16131  subgruhgredgdm  16140  subumgredg2en  16141  subupgr  16143  p1evtxdeqfilem  16181  wlklenvm1  16211  wlklenvm1g  16212  wlkl1loop  16228  upgriswlkdc  16230  uspgr2wlkeq  16235  uspgr2wlkeq2  16236  uspgr2wlkeqi  16237  wlkres  16249  loopclwwlkn1b  16289  clwwlkn1loopb  16290  clwwlkext2edg  16292  clwwlknonccat  16303  s2elclwwlknon2  16306  clwwlknonex2lem2  16308  clwwlknun  16311  eupth2lem3fi  16346  eupth2lembfi  16347  subctctexmid  16652  cvgcmp2nlemabs  16687  trilpolemlt1  16696  gsumgfsumlem  16735  gfsumsn  16737