Theorem eqcomd 2213

Description: Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)

Hypothesis

Ref	Expression
eqcomd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eqcomd	⊢ (𝜑 → 𝐵 = 𝐴)

Proof of Theorem eqcomd

Step	Hyp	Ref	Expression
1		eqcomd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqcom 2209	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	sylib 122	1 ⊢ (𝜑 → 𝐵 = 𝐴)

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 2189

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

This theorem is referenced by:  eqtr2d  2241  eqtr3d  2242  eqtr4d  2243  eqtr2id  2253  eqtr2di  2257  sylan9req  2261  eqeltrrd  2285  eleqtrrd  2287  eleqtrrid  2297  eqeltrrdi  2299  eqnetrrd  2404  neeqtrrd  2408  rspcedeq2vd  2894  dedhb  2949  eqsstrrd  3238  sseqtrrd  3240  eqsstrrdi  3254  dfrab3ss  3459  uneqdifeqim  3554  ifbothdadc  3613  ifbothdc  3614  2if2dc  3619  disjsn2  3706  diftpsn3  3785  elpr2elpr  3830  dfopg  3831  unimax  3898  sndisj  4055  eqbrtrrd  4083  breqtrrd  4087  breqtrrid  4097  eqbrtrrdi  4099  class2seteq  4223  opth1  4298  euotd  4317  opelopabsb  4324  tfisi  4653  0nelxp  4721  opeliunxp  4748  euiotaex  5267  iota4  5270  iotam  5282  fun2ssres  5333  funimass1  5370  funssfv  5625  fnimapr  5662  fvun1  5668  fvco4  5674  elfvmptrab  5698  fmptco  5769  foima2  5843  foeqcnvco  5882  f1eqcocnv  5883  f1oiso2  5919  riotass2  5949  riotass  5950  f1ocnvfv3  5956  fvmpopr2d  6105  caovlem2d  6162  f1opw2  6175  offveq  6202  sbcopeq1a  6296  csbopeq1a  6297  eloprabi  6305  cnvf1olem  6333  f2ndf  6335  smoiso  6411  nnaword  6620  eqer  6675  uniqs  6703  mapsncnv  6805  ixpiinm  6834  mapsnf1o  6847  ssenen  6973  findcard2  7012  findcard2s  7013  unsnfidcex  7043  fisseneq  7057  phpeqd  7058  en1eqsn  7076  sbthlemi6  7090  updjud  7210  omp1eomlem  7222  nnnninf2  7255  nninfisollem0  7258  nninfisollemeq  7260  fodju0  7275  3nsssucpw1  7382  enq0sym  7580  enq0tr  7582  recexgt0sr  7921  caucvgsrlemoffcau  7946  axcaucvglemval  8045  le2tri3i  8216  cnegexlem2  8283  nnpcan  8330  addlsub  8477  negf1o  8489  subdi  8492  rereim  8694  cru  8710  divmulassap  8803  divmulasscomap  8804  divap1d  8909  subhalfhalf  9307  div4p1lem1div2  9326  difgtsumgt  9477  elz2  9479  zindd  9526  qapne  9795  divge1  9880  xrlttri3  9954  fseq1p1m1  10251  fzrevral  10262  nn0disj  10295  fzo0addel  10354  fzosplitsnm1  10375  fzosplitprm1  10400  flqlelt  10456  divfl0  10476  flqpmodeq  10509  zmodidfzo  10535  modqmuladd  10548  qnegmod  10551  addmodid  10554  modifeq2int  10568  modqeqmodmin  10576  modfzo0difsn  10577  modsumfzodifsn  10578  addmodlteq  10580  frecuzrdgsuc  10596  frecfzen2  10609  iseqf1olemab  10684  iseqf1olemmo  10687  seqf1oglem1  10701  seqf1oglem2  10702  ser3sub  10705  expgt1  10759  leexp2r  10775  sqoddm1div8  10875  mulsubdivbinom2ap  10893  bcm1k  10942  bcn2m1  10951  hashinfuni  10959  hashennnuni  10961  hashennn  10962  hashunlem  10986  hashprg  10990  fihashssdif  11000  zfz1isolem1  11022  elovmpowrd  11072  ccatsymb  11096  ccatlid  11100  eqs1  11120  swrdfv2  11154  swrds1  11159  swrdlsw  11160  pfxfv  11175  swrdswrd  11196  swrdpfx  11198  pfxpfx  11199  pfxlswccat  11204  ccats1pfxeq  11205  wrdind  11213  wrd2ind  11214  pfxccatin12lem1  11219  pfxccatin12lem2  11222  swrdccat3blem  11230  swrdccat3b  11231  ccats1pfxeqbi  11233  reuccatpfxs1lem  11237  reuccatpfxs1  11238  shftlem  11242  shftfvalg  11244  shftfval  11247  replim  11285  cjexp  11319  resqrexlemcalc1  11440  resqrexlemcvg  11445  rersqrtthlem  11456  abssq  11507  recan  11535  negfi  11654  minclpr  11663  mingeb  11668  xrmaxiflemcom  11675  xrmineqinf  11695  xrminltinf  11698  xrminadd  11701  climmpt  11726  climrecl  11750  fsum3cvg  11804  summodclem3  11806  summodclem2a  11807  modfsummodlemstep  11883  isumsplit  11917  arisum  11924  geosergap  11932  geo2sum  11940  mertenslemi1  11961  mertenslem2  11962  clim2divap  11966  fproddccvg  11998  fprodssdc  12016  fprodabs  12042  fproddivapf  12057  fprodmodd  12067  efcj  12099  efsub  12107  eflegeo  12127  sinneg  12152  cosneg  12153  sin01bnd  12183  cos01bnd  12184  modm1div  12226  summodnegmod  12248  dvdseq  12274  addmodlteqALT  12285  mulmoddvds  12289  zob  12317  nn0ob  12334  divalgmod  12353  flodddiv4  12362  bitsinv1  12388  divgcdnnr  12412  gcdneg  12418  bezoutlemsup  12445  dvdssq  12467  lcmneg  12511  3lcm2e6woprm  12523  6lcm4e12  12524  divgcdcoprmex  12539  cncongr1  12540  cncongrcoprm  12543  oddpwdclemxy  12606  oddpwdclemodd  12609  divnumden  12633  zgcdsq  12638  phibnd  12654  hashgcdlem  12675  vfermltl  12689  powm2modprm  12690  reumodprminv  12691  pythagtriplem19  12720  pcprendvds2  12729  pczpre  12735  dvdsprmpweqle  12775  difsqpwdvds  12776  4sqlem4  12830  ennnfonelemex  12900  strndxid  12975  topnvalg  13198  prdssca  13222  intopsn  13314  ismgmid2  13327  mgmidsssn0  13331  gsumfzval  13338  gsumprval  13346  mndpfo  13385  mndfo  13386  mndinvmod  13392  prds0g  13396  mnd1id  13403  mhmf1o  13417  0mhm  13433  gsumwmhm  13445  grpidd2  13488  grpinvid2  13500  grpidssd  13523  grpnpcan  13539  grpsubsub4  13540  qusgrp2  13564  mulginvcom  13598  grpissubg  13645  quselbasg  13681  qus0  13686  ecqusaddd  13689  ghmid  13700  ghminv  13701  imasabl  13787  gsumfzmhm  13794  mgpress  13808  rnglz  13822  rngrz  13823  rngmneg1  13824  rngmneg2  13825  rngpropd  13832  srg1zr  13864  srgmulgass  13866  srgpcomp  13867  srgpcomppsc  13869  ringadd2  13904  ringo2times  13905  ringlz  13920  ringrz  13921  ringinvnzdiv  13927  ringnegl  13928  ringnegr  13929  imasring  13941  qusring2  13943  crngunit  13988  rhmopp  14053  lringuplu  14073  opprdomnbg  14151  lmod0vs  14198  lmodvsmmulgdi  14200  lmodfopne  14203  islss3  14256  lspsn  14293  lmodindp1  14305  rnglidlmmgm  14373  rnglidlmsgrp  14374  rnglidlrng  14375  isridl  14381  zringinvg  14481  zndvds  14526  znf1o  14528  psrgrp  14562  toponcom  14614  tgtopon  14653  restopnb  14768  cnptoprest  14826  blfvalps  14972  bdmopn  15091  cnmet  15117  mpomulcn  15153  limcdifap  15249  dvidsslem  15280  dviaddf  15292  dvexp  15298  dvply2g  15353  coseq0negpitopi  15423  abssinper  15433  rplogbzexp  15541  dvdsppwf1o  15576  mpodvdsmulf1o  15577  fsumdvdsmul  15578  sgmmul  15583  perfect  15588  lgsvalmod  15611  lgsneg  15616  gausslemma2dlem1a  15650  gausslemma2dlem6  15659  gausslemma2dlem7  15660  gausslemma2d  15661  lgsquadlem2  15670  2lgslem1a1  15678  2lgslem1a  15680  2lgslem3c  15687  2lgslem3d  15688  2lgslem3d1  15692  2lgs  15696  2lgsoddprm  15705  uhgrun  15797  upgrun  15832  umgrun  15834  subctctexmid  16139  cvgcmp2nlemabs  16173  trilpolemlt1  16182