Theorem eqcomd 2235

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-ext 2211

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

This theorem is referenced by:  eqtr2d  2263  eqtr3d  2264  eqtr4d  2265  eqtr2id  2275  eqtr2di  2279  sylan9req  2283  eqeltrrd  2307  eleqtrrd  2309  eleqtrrid  2319  eqeltrrdi  2321  eqnetrrd  2426  neeqtrrd  2430  rspcedeq2vd  2917  dedhb  2972  eqsstrrd  3261  sseqtrrd  3263  eqsstrrdi  3277  dfrab3ss  3482  uneqdifeqim  3577  ifbothdadc  3636  ifbothdc  3637  2if2dc  3642  disjsn2  3729  diftpsn3  3809  elpr2elpr  3854  dfopg  3855  unimax  3922  sndisj  4079  eqbrtrrd  4107  breqtrrd  4111  breqtrrid  4121  eqbrtrrdi  4123  class2seteq  4248  opth1  4323  euotd  4342  opelopabsb  4349  tfisi  4680  0nelxp  4748  opeliunxp  4776  euiotaex  5298  iota4  5301  iotam  5313  fun2ssres  5364  funimass1  5401  funssfv  5658  fnimapr  5699  fvun1  5705  fvco4  5711  elfvmptrab  5735  fmptco  5806  fncofn  5824  foima2  5884  foeqcnvco  5923  f1eqcocnv  5924  f1oiso2  5960  riotass2  5992  riotass  5993  f1ocnvfv3  5999  fvmpopr2d  6150  caovlem2d  6207  f1opw2  6221  offveq  6248  sbcopeq1a  6342  csbopeq1a  6343  eloprabi  6353  cnvf1olem  6381  f2ndf  6383  smoiso  6459  nnaword  6670  eqer  6725  uniqs  6753  mapsncnv  6855  ixpiinm  6884  mapsnf1o  6897  ssenen  7025  findcard2  7064  findcard2s  7065  unsnfidcex  7098  fisseneq  7112  phpeqd  7113  en1eqsn  7131  sbthlemi6  7145  updjud  7265  omp1eomlem  7277  nnnninf2  7310  nninfisollem0  7313  nninfisollemeq  7315  fodju0  7330  3nsssucpw1  7437  enq0sym  7635  enq0tr  7637  recexgt0sr  7976  caucvgsrlemoffcau  8001  axcaucvglemval  8100  le2tri3i  8271  cnegexlem2  8338  nnpcan  8385  addlsub  8532  negf1o  8544  subdi  8547  rereim  8749  cru  8765  divmulassap  8858  divmulasscomap  8859  divap1d  8964  subhalfhalf  9362  div4p1lem1div2  9381  difgtsumgt  9532  elz2  9534  zindd  9581  qapne  9851  divge1  9936  xrlttri3  10010  fseq1p1m1  10307  fzrevral  10318  nn0disj  10351  fzo0addel  10411  fzosplitsnm1  10432  fzosplitprm1  10457  flqlelt  10513  divfl0  10533  flqpmodeq  10566  zmodidfzo  10592  modqmuladd  10605  qnegmod  10608  addmodid  10611  modifeq2int  10625  modqeqmodmin  10633  modfzo0difsn  10634  modsumfzodifsn  10635  addmodlteq  10637  frecuzrdgsuc  10653  frecfzen2  10666  iseqf1olemab  10741  iseqf1olemmo  10744  seqf1oglem1  10758  seqf1oglem2  10759  ser3sub  10762  expgt1  10816  leexp2r  10832  sqoddm1div8  10932  mulsubdivbinom2ap  10950  bcm1k  10999  bcn2m1  11008  hashinfuni  11016  hashennnuni  11018  hashennn  11019  hashunlem  11043  hashprg  11048  fihashssdif  11058  zfz1isolem1  11080  elovmpowrd  11131  ccatsymb  11155  ccatlid  11159  eqs1  11181  swrdfv2  11216  swrds1  11221  swrdlsw  11222  pfxfv  11237  swrdswrd  11258  swrdpfx  11260  pfxpfx  11261  pfxlswccat  11266  ccats1pfxeq  11267  wrdind  11275  wrd2ind  11276  pfxccatin12lem1  11281  pfxccatin12lem2  11284  swrdccat3blem  11292  swrdccat3b  11293  ccats1pfxeqbi  11295  reuccatpfxs1lem  11299  reuccatpfxs1  11300  shftlem  11348  shftfvalg  11350  shftfval  11353  replim  11391  cjexp  11425  resqrexlemcalc1  11546  resqrexlemcvg  11551  rersqrtthlem  11562  abssq  11613  recan  11641  negfi  11760  minclpr  11769  mingeb  11774  xrmaxiflemcom  11781  xrmineqinf  11801  xrminltinf  11804  xrminadd  11807  climmpt  11832  climrecl  11856  fsum3cvg  11910  summodclem3  11912  summodclem2a  11913  modfsummodlemstep  11989  isumsplit  12023  arisum  12030  geosergap  12038  geo2sum  12046  mertenslemi1  12067  mertenslem2  12068  clim2divap  12072  fproddccvg  12104  fprodssdc  12122  fprodabs  12148  fproddivapf  12163  fprodmodd  12173  efcj  12205  efsub  12213  eflegeo  12233  sinneg  12258  cosneg  12259  sin01bnd  12289  cos01bnd  12290  modm1div  12332  summodnegmod  12354  dvdseq  12380  addmodlteqALT  12391  mulmoddvds  12395  zob  12423  nn0ob  12440  divalgmod  12459  flodddiv4  12468  bitsinv1  12494  divgcdnnr  12518  gcdneg  12524  bezoutlemsup  12551  dvdssq  12573  lcmneg  12617  3lcm2e6woprm  12629  6lcm4e12  12630  divgcdcoprmex  12645  cncongr1  12646  cncongrcoprm  12649  oddpwdclemxy  12712  oddpwdclemodd  12715  divnumden  12739  zgcdsq  12744  phibnd  12760  hashgcdlem  12781  vfermltl  12795  powm2modprm  12796  reumodprminv  12797  pythagtriplem19  12826  pcprendvds2  12835  pczpre  12841  dvdsprmpweqle  12881  difsqpwdvds  12882  4sqlem4  12936  ennnfonelemex  13006  strndxid  13081  topnvalg  13305  prdssca  13329  intopsn  13421  ismgmid2  13434  mgmidsssn0  13438  gsumfzval  13445  gsumprval  13453  mndpfo  13492  mndfo  13493  mndinvmod  13499  prds0g  13503  mnd1id  13510  mhmf1o  13524  0mhm  13540  gsumwmhm  13552  grpidd2  13595  grpinvid2  13607  grpidssd  13630  grpnpcan  13646  grpsubsub4  13647  qusgrp2  13671  mulginvcom  13705  grpissubg  13752  quselbasg  13788  qus0  13793  ecqusaddd  13796  ghmid  13807  ghminv  13808  imasabl  13894  gsumfzmhm  13901  mgpress  13915  rnglz  13929  rngrz  13930  rngmneg1  13931  rngmneg2  13932  rngpropd  13939  srg1zr  13971  srgmulgass  13973  srgpcomp  13974  srgpcomppsc  13976  ringadd2  14011  ringo2times  14012  ringlz  14027  ringrz  14028  ringinvnzdiv  14034  ringnegl  14035  ringnegr  14036  imasring  14048  qusring2  14050  crngunit  14096  rhmopp  14161  lringuplu  14181  opprdomnbg  14259  lmod0vs  14306  lmodvsmmulgdi  14308  lmodfopne  14311  islss3  14364  lspsn  14401  lmodindp1  14413  rnglidlmmgm  14481  rnglidlmsgrp  14482  rnglidlrng  14483  isridl  14489  zringinvg  14589  zndvds  14634  znf1o  14636  psrgrp  14670  toponcom  14722  tgtopon  14761  restopnb  14876  cnptoprest  14934  blfvalps  15080  bdmopn  15199  cnmet  15225  mpomulcn  15261  limcdifap  15357  dvidsslem  15388  dviaddf  15400  dvexp  15406  dvply2g  15461  coseq0negpitopi  15531  abssinper  15541  rplogbzexp  15649  dvdsppwf1o  15684  mpodvdsmulf1o  15685  fsumdvdsmul  15686  sgmmul  15691  perfect  15696  lgsvalmod  15719  lgsneg  15724  gausslemma2dlem1a  15758  gausslemma2dlem6  15767  gausslemma2dlem7  15768  gausslemma2d  15769  lgsquadlem2  15778  2lgslem1a1  15786  2lgslem1a  15788  2lgslem3c  15795  2lgslem3d  15796  2lgslem3d1  15800  2lgs  15804  2lgsoddprm  15813  uhgrun  15907  upgrun  15945  umgrun  15947  ushgredgedg  16045  wlklenvm1  16113  wlklenvm1g  16114  wlkl1loop  16130  upgriswlkdc  16132  uspgr2wlkeq  16137  uspgr2wlkeq2  16138  uspgr2wlkeqi  16139  wlkres  16149  loopclwwlkn1b  16187  clwwlkn1loopb  16188  clwwlkext2edg  16190  subctctexmid  16479  cvgcmp2nlemabs  16514  trilpolemlt1  16523