Theorem eqcomd 2212

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

Syntax hints:   -> wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-ext 2188

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

This theorem is referenced by:  eqtr2d  2240  eqtr3d  2241  eqtr4d  2242  eqtr2id  2252  eqtr2di  2256  sylan9req  2260  eqeltrrd  2284  eleqtrrd  2286  eleqtrrid  2296  eqeltrrdi  2298  eqnetrrd  2403  neeqtrrd  2407  rspcedeq2vd  2891  dedhb  2946  eqsstrrd  3234  sseqtrrd  3236  eqsstrrdi  3250  dfrab3ss  3455  uneqdifeqim  3550  ifbothdadc  3609  ifbothdc  3610  disjsn2  3701  diftpsn3  3780  dfopg  3823  unimax  3890  sndisj  4047  eqbrtrrd  4075  breqtrrd  4079  breqtrrid  4089  eqbrtrrdi  4091  class2seteq  4215  opth1  4288  euotd  4307  opelopabsb  4314  tfisi  4643  0nelxp  4711  opeliunxp  4738  euiotaex  5257  iota4  5260  iotam  5272  fun2ssres  5323  funimass1  5360  funssfv  5615  fnimapr  5652  fvun1  5658  fvco4  5664  elfvmptrab  5688  fmptco  5759  foima2  5833  foeqcnvco  5872  f1eqcocnv  5873  f1oiso2  5909  riotass2  5939  riotass  5940  f1ocnvfv3  5946  fvmpopr2d  6095  caovlem2d  6152  f1opw2  6165  offveq  6192  sbcopeq1a  6286  csbopeq1a  6287  eloprabi  6295  cnvf1olem  6323  f2ndf  6325  smoiso  6401  nnaword  6610  eqer  6665  uniqs  6693  mapsncnv  6795  ixpiinm  6824  mapsnf1o  6837  ssenen  6963  findcard2  7001  findcard2s  7002  unsnfidcex  7032  fisseneq  7046  phpeqd  7047  en1eqsn  7065  sbthlemi6  7079  updjud  7199  omp1eomlem  7211  nnnninf2  7244  nninfisollem0  7247  nninfisollemeq  7249  fodju0  7264  3nsssucpw1  7367  enq0sym  7565  enq0tr  7567  recexgt0sr  7906  caucvgsrlemoffcau  7931  axcaucvglemval  8030  le2tri3i  8201  cnegexlem2  8268  nnpcan  8315  addlsub  8462  negf1o  8474  subdi  8477  rereim  8679  cru  8695  divmulassap  8788  divmulasscomap  8789  divap1d  8894  subhalfhalf  9292  div4p1lem1div2  9311  difgtsumgt  9462  elz2  9464  zindd  9511  qapne  9780  divge1  9865  xrlttri3  9939  fseq1p1m1  10236  fzrevral  10247  nn0disj  10280  fzo0addel  10339  fzosplitsnm1  10360  fzosplitprm1  10385  flqlelt  10441  divfl0  10461  flqpmodeq  10494  zmodidfzo  10520  modqmuladd  10533  qnegmod  10536  addmodid  10539  modifeq2int  10553  modqeqmodmin  10561  modfzo0difsn  10562  modsumfzodifsn  10563  addmodlteq  10565  frecuzrdgsuc  10581  frecfzen2  10594  iseqf1olemab  10669  iseqf1olemmo  10672  seqf1oglem1  10686  seqf1oglem2  10687  ser3sub  10690  expgt1  10744  leexp2r  10760  sqoddm1div8  10860  mulsubdivbinom2ap  10878  bcm1k  10927  bcn2m1  10936  hashinfuni  10944  hashennnuni  10946  hashennn  10947  hashunlem  10971  hashprg  10975  fihashssdif  10985  zfz1isolem1  11007  elovmpowrd  11057  ccatsymb  11081  ccatlid  11085  eqs1  11105  swrdfv2  11139  swrds1  11144  swrdlsw  11145  pfxfv  11160  swrdswrd  11181  swrdpfx  11183  pfxpfx  11184  pfxlswccat  11189  ccats1pfxeq  11190  wrdind  11198  wrd2ind  11199  shftlem  11202  shftfvalg  11204  shftfval  11207  replim  11245  cjexp  11279  resqrexlemcalc1  11400  resqrexlemcvg  11405  rersqrtthlem  11416  abssq  11467  recan  11495  negfi  11614  minclpr  11623  mingeb  11628  xrmaxiflemcom  11635  xrmineqinf  11655  xrminltinf  11658  xrminadd  11661  climmpt  11686  climrecl  11710  fsum3cvg  11764  summodclem3  11766  summodclem2a  11767  modfsummodlemstep  11843  isumsplit  11877  arisum  11884  geosergap  11892  geo2sum  11900  mertenslemi1  11921  mertenslem2  11922  clim2divap  11926  fproddccvg  11958  fprodssdc  11976  fprodabs  12002  fproddivapf  12017  fprodmodd  12027  efcj  12059  efsub  12067  eflegeo  12087  sinneg  12112  cosneg  12113  sin01bnd  12143  cos01bnd  12144  modm1div  12186  summodnegmod  12208  dvdseq  12234  addmodlteqALT  12245  mulmoddvds  12249  zob  12277  nn0ob  12294  divalgmod  12313  flodddiv4  12322  bitsinv1  12348  divgcdnnr  12372  gcdneg  12378  bezoutlemsup  12405  dvdssq  12427  lcmneg  12471  3lcm2e6woprm  12483  6lcm4e12  12484  divgcdcoprmex  12499  cncongr1  12500  cncongrcoprm  12503  oddpwdclemxy  12566  oddpwdclemodd  12569  divnumden  12593  zgcdsq  12598  phibnd  12614  hashgcdlem  12635  vfermltl  12649  powm2modprm  12650  reumodprminv  12651  pythagtriplem19  12680  pcprendvds2  12689  pczpre  12695  dvdsprmpweqle  12735  difsqpwdvds  12736  4sqlem4  12790  ennnfonelemex  12860  strndxid  12935  topnvalg  13158  prdssca  13182  intopsn  13274  ismgmid2  13287  mgmidsssn0  13291  gsumfzval  13298  gsumprval  13306  mndpfo  13345  mndfo  13346  mndinvmod  13352  prds0g  13356  mnd1id  13363  mhmf1o  13377  0mhm  13393  gsumwmhm  13405  grpidd2  13448  grpinvid2  13460  grpidssd  13483  grpnpcan  13499  grpsubsub4  13500  qusgrp2  13524  mulginvcom  13558  grpissubg  13605  quselbasg  13641  qus0  13646  ecqusaddd  13649  ghmid  13660  ghminv  13661  imasabl  13747  gsumfzmhm  13754  mgpress  13768  rnglz  13782  rngrz  13783  rngmneg1  13784  rngmneg2  13785  rngpropd  13792  srg1zr  13824  srgmulgass  13826  srgpcomp  13827  srgpcomppsc  13829  ringadd2  13864  ringo2times  13865  ringlz  13880  ringrz  13881  ringinvnzdiv  13887  ringnegl  13888  ringnegr  13889  imasring  13901  qusring2  13903  crngunit  13948  rhmopp  14013  lringuplu  14033  opprdomnbg  14111  lmod0vs  14158  lmodvsmmulgdi  14160  lmodfopne  14163  islss3  14216  lspsn  14253  lmodindp1  14265  rnglidlmmgm  14333  rnglidlmsgrp  14334  rnglidlrng  14335  isridl  14341  zringinvg  14441  zndvds  14486  znf1o  14488  psrgrp  14522  toponcom  14574  tgtopon  14613  restopnb  14728  cnptoprest  14786  blfvalps  14932  bdmopn  15051  cnmet  15077  mpomulcn  15113  limcdifap  15209  dvidsslem  15240  dviaddf  15252  dvexp  15258  dvply2g  15313  coseq0negpitopi  15383  abssinper  15393  rplogbzexp  15501  dvdsppwf1o  15536  mpodvdsmulf1o  15537  fsumdvdsmul  15538  sgmmul  15543  perfect  15548  lgsvalmod  15571  lgsneg  15576  gausslemma2dlem1a  15610  gausslemma2dlem6  15619  gausslemma2dlem7  15620  gausslemma2d  15621  lgsquadlem2  15630  2lgslem1a1  15638  2lgslem1a  15640  2lgslem3c  15647  2lgslem3d  15648  2lgslem3d1  15652  2lgs  15656  2lgsoddprm  15665  uhgrun  15757  upgrun  15792  umgrun  15794  subctctexmid  16078  cvgcmp2nlemabs  16112  trilpolemlt1  16121