Theorem eqcomd 2146

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 2142	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	sylib 121	1 ⊢ (𝜑 → 𝐵 = 𝐴)

Syntax hints:   → wi 4   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  eqtr2d  2174  eqtr3d  2175  eqtr4d  2176  syl5req  2186  eqtr2di  2190  sylan9req  2194  eqeltrrd  2218  eleqtrrd  2220  eleqtrrid  2230  eqeltrrdi  2232  eqnetrrd  2335  neeqtrrd  2339  rspcedeq2vd  2803  dedhb  2857  eqsstrrd  3139  sseqtrrd  3141  eqsstrrdi  3155  dfrab3ss  3359  uneqdifeqim  3453  ifbothdadc  3508  ifbothdc  3509  disjsn2  3594  diftpsn3  3669  dfopg  3711  unimax  3778  sndisj  3933  eqbrtrrd  3960  breqtrrd  3964  breqtrrid  3974  eqbrtrrdi  3976  class2seteq  4095  opth1  4166  euotd  4184  opelopabsb  4190  tfisi  4509  0nelxp  4575  opeliunxp  4602  euiotaex  5112  iota4  5114  fun2ssres  5174  funimass1  5208  funssfv  5455  fnimapr  5489  fvun1  5495  fvco4  5501  elfvmptrab  5524  fmptco  5594  foima2  5661  foeqcnvco  5699  f1eqcocnv  5700  f1oiso2  5736  riotass2  5764  riotass  5765  f1ocnvfv3  5771  caovlem2d  5971  f1opw2  5984  sbcopeq1a  6093  csbopeq1a  6094  eloprabi  6102  cnvf1olem  6129  f2ndf  6131  smoiso  6207  nnaword  6415  eqer  6469  uniqs  6495  mapsncnv  6597  ixpiinm  6626  mapsnf1o  6639  ssenen  6753  findcard2  6791  findcard2s  6792  unsnfidcex  6816  fisseneq  6828  phpeqd  6829  en1eqsn  6844  sbthlemi6  6858  updjud  6975  omp1eomlem  6987  fodju0  7027  enq0sym  7264  enq0tr  7266  recexgt0sr  7605  caucvgsrlemoffcau  7630  axcaucvglemval  7729  le2tri3i  7896  cnegexlem2  7962  nnpcan  8009  addlsub  8156  negf1o  8168  subdi  8171  rereim  8372  cru  8388  divmulassap  8479  divmulasscomap  8480  divap1d  8585  div4p1lem1div2  8997  elz2  9146  zindd  9193  qapne  9458  divge1  9540  xrlttri3  9613  fseq1p1m1  9905  fzrevral  9916  nn0disj  9946  fzosplitsnm1  10017  fzosplitprm1  10042  flqlelt  10080  divfl0  10100  flqpmodeq  10131  zmodidfzo  10157  modqmuladd  10170  qnegmod  10173  addmodid  10176  modifeq2int  10190  modqeqmodmin  10198  modfzo0difsn  10199  modsumfzodifsn  10200  addmodlteq  10202  frecuzrdgsuc  10218  frecfzen2  10231  iseqf1olemab  10293  iseqf1olemmo  10296  ser3sub  10310  expgt1  10362  leexp2r  10378  sqoddm1div8  10475  bcm1k  10538  bcn2m1  10547  hashinfuni  10555  hashennnuni  10557  hashennn  10558  hashunlem  10582  hashprg  10586  fihashssdif  10596  zfz1isolem1  10615  shftlem  10620  shftfvalg  10622  shftfval  10625  replim  10663  cjexp  10697  resqrexlemcalc1  10818  resqrexlemcvg  10823  rersqrtthlem  10834  abssq  10885  recan  10913  negfi  11031  minclpr  11040  xrmaxiflemcom  11050  xrmineqinf  11070  xrminltinf  11073  xrminadd  11076  climmpt  11101  climrecl  11125  fsum3cvg  11179  summodclem3  11181  summodclem2a  11182  modfsummodlemstep  11258  isumsplit  11292  arisum  11299  geosergap  11307  geo2sum  11315  mertenslemi1  11336  mertenslem2  11337  clim2divap  11341  fproddccvg  11373  efcj  11416  efsub  11424  eflegeo  11444  sinneg  11469  cosneg  11470  sin01bnd  11500  cos01bnd  11501  summodnegmod  11560  dvdseq  11582  addmodlteqALT  11593  mulmoddvds  11597  zob  11624  nn0ob  11641  divalgmod  11660  flodddiv4  11667  divgcdnnr  11700  gcdneg  11706  bezoutlemsup  11733  dvdssq  11755  lcmneg  11791  3lcm2e6woprm  11803  6lcm4e12  11804  divgcdcoprmex  11819  cncongr1  11820  cncongrcoprm  11823  oddpwdclemxy  11883  oddpwdclemodd  11886  divnumden  11910  zgcdsq  11915  phibnd  11929  hashgcdlem  11939  ennnfonelemex  11963  strndxid  12026  topnvalg  12171  toponcom  12233  tgtopon  12274  restopnb  12389  cnptoprest  12447  blfvalps  12593  bdmopn  12712  cnmet  12738  limcdifap  12839  dviaddf  12877  dvexp  12883  coseq0negpitopi  12965  abssinper  12975  rplogbzexp  13079  subctctexmid  13369  cvgcmp2nlemabs  13402  trilpolemlt1  13409