Theorem eqcomd 2199

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-ext 2175

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

This theorem is referenced by:  eqtr2d  2227  eqtr3d  2228  eqtr4d  2229  eqtr2id  2239  eqtr2di  2243  sylan9req  2247  eqeltrrd  2271  eleqtrrd  2273  eleqtrrid  2283  eqeltrrdi  2285  eqnetrrd  2390  neeqtrrd  2394  rspcedeq2vd  2875  dedhb  2930  eqsstrrd  3217  sseqtrrd  3219  eqsstrrdi  3233  dfrab3ss  3438  uneqdifeqim  3533  ifbothdadc  3590  ifbothdc  3591  disjsn2  3682  diftpsn3  3760  dfopg  3803  unimax  3870  sndisj  4026  eqbrtrrd  4054  breqtrrd  4058  breqtrrid  4068  eqbrtrrdi  4070  class2seteq  4193  opth1  4266  euotd  4284  opelopabsb  4291  tfisi  4620  0nelxp  4688  opeliunxp  4715  euiotaex  5232  iota4  5235  iotam  5247  fun2ssres  5298  funimass1  5332  funssfv  5581  fnimapr  5618  fvun1  5624  fvco4  5630  elfvmptrab  5654  fmptco  5725  foima2  5795  foeqcnvco  5834  f1eqcocnv  5835  f1oiso2  5871  riotass2  5901  riotass  5902  f1ocnvfv3  5908  fvmpopr2d  6056  caovlem2d  6113  f1opw2  6126  sbcopeq1a  6242  csbopeq1a  6243  eloprabi  6251  cnvf1olem  6279  f2ndf  6281  smoiso  6357  nnaword  6566  eqer  6621  uniqs  6649  mapsncnv  6751  ixpiinm  6780  mapsnf1o  6793  ssenen  6909  findcard2  6947  findcard2s  6948  unsnfidcex  6978  fisseneq  6990  phpeqd  6991  en1eqsn  7009  sbthlemi6  7023  updjud  7143  omp1eomlem  7155  nnnninf2  7188  nninfisollem0  7191  nninfisollemeq  7193  fodju0  7208  3nsssucpw1  7298  enq0sym  7494  enq0tr  7496  recexgt0sr  7835  caucvgsrlemoffcau  7860  axcaucvglemval  7959  le2tri3i  8130  cnegexlem2  8197  nnpcan  8244  addlsub  8391  negf1o  8403  subdi  8406  rereim  8607  cru  8623  divmulassap  8716  divmulasscomap  8717  divap1d  8822  subhalfhalf  9220  div4p1lem1div2  9239  difgtsumgt  9389  elz2  9391  zindd  9438  qapne  9707  divge1  9792  xrlttri3  9866  fseq1p1m1  10163  fzrevral  10174  nn0disj  10207  fzosplitsnm1  10279  fzosplitprm1  10304  flqlelt  10348  divfl0  10368  flqpmodeq  10401  zmodidfzo  10427  modqmuladd  10440  qnegmod  10443  addmodid  10446  modifeq2int  10460  modqeqmodmin  10468  modfzo0difsn  10469  modsumfzodifsn  10470  addmodlteq  10472  frecuzrdgsuc  10488  frecfzen2  10501  iseqf1olemab  10576  iseqf1olemmo  10579  seqf1oglem1  10593  seqf1oglem2  10594  ser3sub  10597  expgt1  10651  leexp2r  10667  sqoddm1div8  10767  mulsubdivbinom2ap  10785  bcm1k  10834  bcn2m1  10843  hashinfuni  10851  hashennnuni  10853  hashennn  10854  hashunlem  10878  hashprg  10882  fihashssdif  10892  zfz1isolem1  10914  elovmpowrd  10958  shftlem  10963  shftfvalg  10965  shftfval  10968  replim  11006  cjexp  11040  resqrexlemcalc1  11161  resqrexlemcvg  11166  rersqrtthlem  11177  abssq  11228  recan  11256  negfi  11374  minclpr  11383  mingeb  11388  xrmaxiflemcom  11395  xrmineqinf  11415  xrminltinf  11418  xrminadd  11421  climmpt  11446  climrecl  11470  fsum3cvg  11524  summodclem3  11526  summodclem2a  11527  modfsummodlemstep  11603  isumsplit  11637  arisum  11644  geosergap  11652  geo2sum  11660  mertenslemi1  11681  mertenslem2  11682  clim2divap  11686  fproddccvg  11718  fprodssdc  11736  fprodabs  11762  fproddivapf  11777  fprodmodd  11787  efcj  11819  efsub  11827  eflegeo  11847  sinneg  11872  cosneg  11873  sin01bnd  11903  cos01bnd  11904  modm1div  11946  summodnegmod  11968  dvdseq  11993  addmodlteqALT  12004  mulmoddvds  12008  zob  12035  nn0ob  12052  divalgmod  12071  flodddiv4  12078  divgcdnnr  12116  gcdneg  12122  bezoutlemsup  12149  dvdssq  12171  lcmneg  12215  3lcm2e6woprm  12227  6lcm4e12  12228  divgcdcoprmex  12243  cncongr1  12244  cncongrcoprm  12247  oddpwdclemxy  12310  oddpwdclemodd  12313  divnumden  12337  zgcdsq  12342  phibnd  12358  hashgcdlem  12379  vfermltl  12392  powm2modprm  12393  reumodprminv  12394  pythagtriplem19  12423  pcprendvds2  12432  pczpre  12438  dvdsprmpweqle  12478  difsqpwdvds  12479  4sqlem4  12533  ennnfonelemex  12574  strndxid  12649  topnvalg  12865  intopsn  12953  ismgmid2  12966  mgmidsssn0  12970  gsumfzval  12977  gsumprval  12985  mndpfo  13022  mndfo  13023  mndinvmod  13029  mnd1id  13031  mhmf1o  13045  0mhm  13061  gsumwmhm  13073  grpidd2  13116  grpinvid2  13128  grpidssd  13151  grpnpcan  13167  grpsubsub4  13168  qusgrp2  13186  mulginvcom  13220  grpissubg  13267  quselbasg  13303  qus0  13308  ecqusaddd  13311  ghmid  13322  ghminv  13323  imasabl  13409  gsumfzmhm  13416  mgpress  13430  rnglz  13444  rngrz  13445  rngmneg1  13446  rngmneg2  13447  rngpropd  13454  srg1zr  13486  srgmulgass  13488  srgpcomp  13489  srgpcomppsc  13491  ringadd2  13526  ringo2times  13527  ringlz  13542  ringrz  13543  ringinvnzdiv  13549  ringnegl  13550  ringnegr  13551  imasring  13563  qusring2  13565  crngunit  13610  rhmopp  13675  lringuplu  13695  opprdomnbg  13773  lmod0vs  13820  lmodvsmmulgdi  13822  lmodfopne  13825  islss3  13878  lspsn  13915  lmodindp1  13927  rnglidlmmgm  13995  rnglidlmsgrp  13996  rnglidlrng  13997  isridl  14003  zringinvg  14103  zndvds  14148  znf1o  14150  toponcom  14206  tgtopon  14245  restopnb  14360  cnptoprest  14418  blfvalps  14564  bdmopn  14683  cnmet  14709  mpomulcn  14745  limcdifap  14841  dvidsslem  14872  dviaddf  14884  dvexp  14890  coseq0negpitopi  15012  abssinper  15022  rplogbzexp  15127  lgsvalmod  15176  lgsneg  15181  gausslemma2dlem1a  15215  gausslemma2dlem6  15224  gausslemma2dlem7  15225  gausslemma2d  15226  lgsquadlem2  15235  2lgslem1a1  15243  2lgslem1a  15245  2lgslem3c  15252  2lgslem3d  15253  2lgslem3d1  15257  2lgs  15261  2lgsoddprm  15270  subctctexmid  15561  cvgcmp2nlemabs  15592  trilpolemlt1  15601