Theorem eqcomd 2215

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

Syntax hints:   → wi 4   = wceq 1375

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 1473  ax-gen 1475  ax-ext 2191

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

This theorem is referenced by:  eqtr2d  2243  eqtr3d  2244  eqtr4d  2245  eqtr2id  2255  eqtr2di  2259  sylan9req  2263  eqeltrrd  2287  eleqtrrd  2289  eleqtrrid  2299  eqeltrrdi  2301  eqnetrrd  2406  neeqtrrd  2410  rspcedeq2vd  2897  dedhb  2952  eqsstrrd  3241  sseqtrrd  3243  eqsstrrdi  3257  dfrab3ss  3462  uneqdifeqim  3557  ifbothdadc  3616  ifbothdc  3617  2if2dc  3622  disjsn2  3709  diftpsn3  3788  elpr2elpr  3833  dfopg  3834  unimax  3901  sndisj  4058  eqbrtrrd  4086  breqtrrd  4090  breqtrrid  4100  eqbrtrrdi  4102  class2seteq  4226  opth1  4301  euotd  4320  opelopabsb  4327  tfisi  4656  0nelxp  4724  opeliunxp  4751  euiotaex  5271  iota4  5274  iotam  5286  fun2ssres  5337  funimass1  5374  funssfv  5629  fnimapr  5667  fvun1  5673  fvco4  5679  elfvmptrab  5703  fmptco  5774  foima2  5848  foeqcnvco  5887  f1eqcocnv  5888  f1oiso2  5924  riotass2  5956  riotass  5957  f1ocnvfv3  5963  fvmpopr2d  6112  caovlem2d  6169  f1opw2  6182  offveq  6209  sbcopeq1a  6303  csbopeq1a  6304  eloprabi  6312  cnvf1olem  6340  f2ndf  6342  smoiso  6418  nnaword  6627  eqer  6682  uniqs  6710  mapsncnv  6812  ixpiinm  6841  mapsnf1o  6854  ssenen  6980  findcard2  7019  findcard2s  7020  unsnfidcex  7050  fisseneq  7064  phpeqd  7065  en1eqsn  7083  sbthlemi6  7097  updjud  7217  omp1eomlem  7229  nnnninf2  7262  nninfisollem0  7265  nninfisollemeq  7267  fodju0  7282  3nsssucpw1  7389  enq0sym  7587  enq0tr  7589  recexgt0sr  7928  caucvgsrlemoffcau  7953  axcaucvglemval  8052  le2tri3i  8223  cnegexlem2  8290  nnpcan  8337  addlsub  8484  negf1o  8496  subdi  8499  rereim  8701  cru  8717  divmulassap  8810  divmulasscomap  8811  divap1d  8916  subhalfhalf  9314  div4p1lem1div2  9333  difgtsumgt  9484  elz2  9486  zindd  9533  qapne  9802  divge1  9887  xrlttri3  9961  fseq1p1m1  10258  fzrevral  10269  nn0disj  10302  fzo0addel  10361  fzosplitsnm1  10382  fzosplitprm1  10407  flqlelt  10463  divfl0  10483  flqpmodeq  10516  zmodidfzo  10542  modqmuladd  10555  qnegmod  10558  addmodid  10561  modifeq2int  10575  modqeqmodmin  10583  modfzo0difsn  10584  modsumfzodifsn  10585  addmodlteq  10587  frecuzrdgsuc  10603  frecfzen2  10616  iseqf1olemab  10691  iseqf1olemmo  10694  seqf1oglem1  10708  seqf1oglem2  10709  ser3sub  10712  expgt1  10766  leexp2r  10782  sqoddm1div8  10882  mulsubdivbinom2ap  10900  bcm1k  10949  bcn2m1  10958  hashinfuni  10966  hashennnuni  10968  hashennn  10969  hashunlem  10993  hashprg  10997  fihashssdif  11007  zfz1isolem1  11029  elovmpowrd  11079  ccatsymb  11103  ccatlid  11107  eqs1  11127  swrdfv2  11161  swrds1  11166  swrdlsw  11167  pfxfv  11182  swrdswrd  11203  swrdpfx  11205  pfxpfx  11206  pfxlswccat  11211  ccats1pfxeq  11212  wrdind  11220  wrd2ind  11221  pfxccatin12lem1  11226  pfxccatin12lem2  11229  swrdccat3blem  11237  swrdccat3b  11238  ccats1pfxeqbi  11240  reuccatpfxs1lem  11244  reuccatpfxs1  11245  shftlem  11293  shftfvalg  11295  shftfval  11298  replim  11336  cjexp  11370  resqrexlemcalc1  11491  resqrexlemcvg  11496  rersqrtthlem  11507  abssq  11558  recan  11586  negfi  11705  minclpr  11714  mingeb  11719  xrmaxiflemcom  11726  xrmineqinf  11746  xrminltinf  11749  xrminadd  11752  climmpt  11777  climrecl  11801  fsum3cvg  11855  summodclem3  11857  summodclem2a  11858  modfsummodlemstep  11934  isumsplit  11968  arisum  11975  geosergap  11983  geo2sum  11991  mertenslemi1  12012  mertenslem2  12013  clim2divap  12017  fproddccvg  12049  fprodssdc  12067  fprodabs  12093  fproddivapf  12108  fprodmodd  12118  efcj  12150  efsub  12158  eflegeo  12178  sinneg  12203  cosneg  12204  sin01bnd  12234  cos01bnd  12235  modm1div  12277  summodnegmod  12299  dvdseq  12325  addmodlteqALT  12336  mulmoddvds  12340  zob  12368  nn0ob  12385  divalgmod  12404  flodddiv4  12413  bitsinv1  12439  divgcdnnr  12463  gcdneg  12469  bezoutlemsup  12496  dvdssq  12518  lcmneg  12562  3lcm2e6woprm  12574  6lcm4e12  12575  divgcdcoprmex  12590  cncongr1  12591  cncongrcoprm  12594  oddpwdclemxy  12657  oddpwdclemodd  12660  divnumden  12684  zgcdsq  12689  phibnd  12705  hashgcdlem  12726  vfermltl  12740  powm2modprm  12741  reumodprminv  12742  pythagtriplem19  12771  pcprendvds2  12780  pczpre  12786  dvdsprmpweqle  12826  difsqpwdvds  12827  4sqlem4  12881  ennnfonelemex  12951  strndxid  13026  topnvalg  13250  prdssca  13274  intopsn  13366  ismgmid2  13379  mgmidsssn0  13383  gsumfzval  13390  gsumprval  13398  mndpfo  13437  mndfo  13438  mndinvmod  13444  prds0g  13448  mnd1id  13455  mhmf1o  13469  0mhm  13485  gsumwmhm  13497  grpidd2  13540  grpinvid2  13552  grpidssd  13575  grpnpcan  13591  grpsubsub4  13592  qusgrp2  13616  mulginvcom  13650  grpissubg  13697  quselbasg  13733  qus0  13738  ecqusaddd  13741  ghmid  13752  ghminv  13753  imasabl  13839  gsumfzmhm  13846  mgpress  13860  rnglz  13874  rngrz  13875  rngmneg1  13876  rngmneg2  13877  rngpropd  13884  srg1zr  13916  srgmulgass  13918  srgpcomp  13919  srgpcomppsc  13921  ringadd2  13956  ringo2times  13957  ringlz  13972  ringrz  13973  ringinvnzdiv  13979  ringnegl  13980  ringnegr  13981  imasring  13993  qusring2  13995  crngunit  14040  rhmopp  14105  lringuplu  14125  opprdomnbg  14203  lmod0vs  14250  lmodvsmmulgdi  14252  lmodfopne  14255  islss3  14308  lspsn  14345  lmodindp1  14357  rnglidlmmgm  14425  rnglidlmsgrp  14426  rnglidlrng  14427  isridl  14433  zringinvg  14533  zndvds  14578  znf1o  14580  psrgrp  14614  toponcom  14666  tgtopon  14705  restopnb  14820  cnptoprest  14878  blfvalps  15024  bdmopn  15143  cnmet  15169  mpomulcn  15205  limcdifap  15301  dvidsslem  15332  dviaddf  15344  dvexp  15350  dvply2g  15405  coseq0negpitopi  15475  abssinper  15485  rplogbzexp  15593  dvdsppwf1o  15628  mpodvdsmulf1o  15629  fsumdvdsmul  15630  sgmmul  15635  perfect  15640  lgsvalmod  15663  lgsneg  15668  gausslemma2dlem1a  15702  gausslemma2dlem6  15711  gausslemma2dlem7  15712  gausslemma2d  15713  lgsquadlem2  15722  2lgslem1a1  15730  2lgslem1a  15732  2lgslem3c  15739  2lgslem3d  15740  2lgslem3d1  15744  2lgs  15748  2lgsoddprm  15757  uhgrun  15851  upgrun  15889  umgrun  15891  ushgredgedg  15989  subctctexmid  16277  cvgcmp2nlemabs  16311  trilpolemlt1  16320