Theorem eqcomd 2195

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 2191	. 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 2171

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

This theorem is referenced by:  eqtr2d  2223  eqtr3d  2224  eqtr4d  2225  eqtr2id  2235  eqtr2di  2239  sylan9req  2243  eqeltrrd  2267  eleqtrrd  2269  eleqtrrid  2279  eqeltrrdi  2281  eqnetrrd  2386  neeqtrrd  2390  rspcedeq2vd  2866  dedhb  2921  eqsstrrd  3207  sseqtrrd  3209  eqsstrrdi  3223  dfrab3ss  3428  uneqdifeqim  3523  ifbothdadc  3581  ifbothdc  3582  disjsn2  3670  diftpsn3  3748  dfopg  3791  unimax  3858  sndisj  4014  eqbrtrrd  4042  breqtrrd  4046  breqtrrid  4056  eqbrtrrdi  4058  class2seteq  4181  opth1  4254  euotd  4272  opelopabsb  4278  tfisi  4604  0nelxp  4672  opeliunxp  4699  euiotaex  5212  iota4  5215  iotam  5227  fun2ssres  5278  funimass1  5312  funssfv  5560  fnimapr  5597  fvun1  5603  fvco4  5609  elfvmptrab  5632  fmptco  5703  foima2  5773  foeqcnvco  5812  f1eqcocnv  5813  f1oiso2  5849  riotass2  5879  riotass  5880  f1ocnvfv3  5886  caovlem2d  6090  f1opw2  6101  sbcopeq1a  6213  csbopeq1a  6214  eloprabi  6222  cnvf1olem  6250  f2ndf  6252  smoiso  6328  nnaword  6537  eqer  6592  uniqs  6620  mapsncnv  6722  ixpiinm  6751  mapsnf1o  6764  ssenen  6880  findcard2  6918  findcard2s  6919  unsnfidcex  6949  fisseneq  6961  phpeqd  6962  en1eqsn  6978  sbthlemi6  6992  updjud  7112  omp1eomlem  7124  nnnninf2  7156  nninfisollem0  7159  nninfisollemeq  7161  fodju0  7176  3nsssucpw1  7266  enq0sym  7462  enq0tr  7464  recexgt0sr  7803  caucvgsrlemoffcau  7828  axcaucvglemval  7927  le2tri3i  8097  cnegexlem2  8164  nnpcan  8211  addlsub  8358  negf1o  8370  subdi  8373  rereim  8574  cru  8590  divmulassap  8683  divmulasscomap  8684  divap1d  8789  div4p1lem1div2  9203  difgtsumgt  9353  elz2  9355  zindd  9402  qapne  9671  divge1  9755  xrlttri3  9829  fseq1p1m1  10126  fzrevral  10137  nn0disj  10170  fzosplitsnm1  10241  fzosplitprm1  10266  flqlelt  10309  divfl0  10329  flqpmodeq  10360  zmodidfzo  10386  modqmuladd  10399  qnegmod  10402  addmodid  10405  modifeq2int  10419  modqeqmodmin  10427  modfzo0difsn  10428  modsumfzodifsn  10429  addmodlteq  10431  frecuzrdgsuc  10447  frecfzen2  10460  iseqf1olemab  10522  iseqf1olemmo  10525  ser3sub  10539  expgt1  10592  leexp2r  10608  sqoddm1div8  10708  mulsubdivbinom2ap  10726  bcm1k  10775  bcn2m1  10784  hashinfuni  10792  hashennnuni  10794  hashennn  10795  hashunlem  10819  hashprg  10823  fihashssdif  10833  zfz1isolem1  10855  shftlem  10860  shftfvalg  10862  shftfval  10865  replim  10903  cjexp  10937  resqrexlemcalc1  11058  resqrexlemcvg  11063  rersqrtthlem  11074  abssq  11125  recan  11153  negfi  11271  minclpr  11280  mingeb  11285  xrmaxiflemcom  11292  xrmineqinf  11312  xrminltinf  11315  xrminadd  11318  climmpt  11343  climrecl  11367  fsum3cvg  11421  summodclem3  11423  summodclem2a  11424  modfsummodlemstep  11500  isumsplit  11534  arisum  11541  geosergap  11549  geo2sum  11557  mertenslemi1  11578  mertenslem2  11579  clim2divap  11583  fproddccvg  11615  fprodssdc  11633  fprodabs  11659  fproddivapf  11674  fprodmodd  11684  efcj  11716  efsub  11724  eflegeo  11744  sinneg  11769  cosneg  11770  sin01bnd  11800  cos01bnd  11801  modm1div  11842  summodnegmod  11864  dvdseq  11889  addmodlteqALT  11900  mulmoddvds  11904  zob  11931  nn0ob  11948  divalgmod  11967  flodddiv4  11974  divgcdnnr  12012  gcdneg  12018  bezoutlemsup  12045  dvdssq  12067  lcmneg  12109  3lcm2e6woprm  12121  6lcm4e12  12122  divgcdcoprmex  12137  cncongr1  12138  cncongrcoprm  12141  oddpwdclemxy  12204  oddpwdclemodd  12207  divnumden  12231  zgcdsq  12236  phibnd  12252  hashgcdlem  12273  vfermltl  12286  powm2modprm  12287  reumodprminv  12288  pythagtriplem19  12317  pcprendvds2  12326  pczpre  12332  dvdsprmpweqle  12372  difsqpwdvds  12373  4sqlem4  12427  ennnfonelemex  12468  strndxid  12543  topnvalg  12759  intopsn  12846  ismgmid2  12859  mgmidsssn0  12863  gsumprval  12877  mndpfo  12914  mndfo  12915  mndinvmod  12921  mnd1id  12923  mhmf1o  12937  0mhm  12953  grpidd2  13000  grpinvid2  13012  grpidssd  13035  grpnpcan  13051  grpsubsub4  13052  qusgrp2  13070  mulginvcom  13104  grpissubg  13150  quselbasg  13186  qus0  13191  ecqusaddd  13194  ghmid  13205  ghminv  13206  imasabl  13290  mgpress  13302  rnglz  13316  rngrz  13317  rngmneg1  13318  rngmneg2  13319  rngpropd  13326  srg1zr  13358  srgmulgass  13360  srgpcomp  13361  srgpcomppsc  13363  ringadd2  13398  ringo2times  13399  ringlz  13414  ringrz  13415  ringinvnzdiv  13419  ringnegl  13420  ringnegr  13421  imasring  13431  qusring2  13433  crngunit  13478  rhmopp  13543  lringuplu  13560  lmod0vs  13654  lmodvsmmulgdi  13656  lmodfopne  13659  islss3  13712  lspsn  13749  lmodindp1  13761  rnglidlmmgm  13829  rnglidlmsgrp  13830  rnglidlrng  13831  isridl  13836  zringinvg  13920  toponcom  14004  tgtopon  14043  restopnb  14158  cnptoprest  14216  blfvalps  14362  bdmopn  14481  cnmet  14507  limcdifap  14608  dviaddf  14646  dvexp  14652  coseq0negpitopi  14734  abssinper  14744  rplogbzexp  14849  lgsvalmod  14898  lgsneg  14903  subctctexmid  15229  cvgcmp2nlemabs  15259  trilpolemlt1  15268