Theorem eqcomd 2145

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

Syntax hints:   → wi 4   = wceq 1331

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 1423  ax-gen 1425  ax-ext 2121

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

This theorem is referenced by:  eqtr2d  2173  eqtr3d  2174  eqtr4d  2175  syl5req  2185  syl6req  2189  sylan9req  2193  eqeltrrd  2217  eleqtrrd  2219  eleqtrrid  2229  eqeltrrdi  2231  eqnetrrd  2334  neeqtrrd  2338  rspcedeq2vd  2799  dedhb  2853  eqsstrrd  3134  sseqtrrd  3136  eqsstrrdi  3150  dfrab3ss  3354  uneqdifeqim  3448  ifbothdadc  3503  ifbothdc  3504  disjsn2  3586  diftpsn3  3661  dfopg  3703  unimax  3770  sndisj  3925  eqbrtrrd  3952  breqtrrd  3956  breqtrrid  3966  eqbrtrrdi  3968  class2seteq  4087  opth1  4158  euotd  4176  opelopabsb  4182  tfisi  4501  0nelxp  4567  opeliunxp  4594  euiotaex  5104  iota4  5106  fun2ssres  5166  funimass1  5200  funssfv  5447  fnimapr  5481  fvun1  5487  fvco4  5493  elfvmptrab  5516  fmptco  5586  foima2  5653  foeqcnvco  5691  f1eqcocnv  5692  f1oiso2  5728  riotass2  5756  riotass  5757  f1ocnvfv3  5763  caovlem2d  5963  f1opw2  5976  sbcopeq1a  6085  csbopeq1a  6086  eloprabi  6094  cnvf1olem  6121  f2ndf  6123  smoiso  6199  nnaword  6407  eqer  6461  uniqs  6487  mapsncnv  6589  ixpiinm  6618  mapsnf1o  6631  ssenen  6745  findcard2  6783  findcard2s  6784  unsnfidcex  6808  fisseneq  6820  phpeqd  6821  en1eqsn  6836  sbthlemi6  6850  updjud  6967  omp1eomlem  6979  fodju0  7019  enq0sym  7240  enq0tr  7242  recexgt0sr  7581  caucvgsrlemoffcau  7606  axcaucvglemval  7705  le2tri3i  7872  cnegexlem2  7938  nnpcan  7985  addlsub  8132  negf1o  8144  subdi  8147  rereim  8348  cru  8364  divmulassap  8455  divmulasscomap  8456  divap1d  8561  div4p1lem1div2  8973  elz2  9122  zindd  9169  qapne  9431  divge1  9510  xrlttri3  9583  fseq1p1m1  9874  fzrevral  9885  nn0disj  9915  fzosplitsnm1  9986  fzosplitprm1  10011  flqlelt  10049  divfl0  10069  flqpmodeq  10100  zmodidfzo  10126  modqmuladd  10139  qnegmod  10142  addmodid  10145  modifeq2int  10159  modqeqmodmin  10167  modfzo0difsn  10168  modsumfzodifsn  10169  addmodlteq  10171  frecuzrdgsuc  10187  frecfzen2  10200  iseqf1olemab  10262  iseqf1olemmo  10265  ser3sub  10279  expgt1  10331  leexp2r  10347  sqoddm1div8  10444  bcm1k  10506  bcn2m1  10515  hashinfuni  10523  hashennnuni  10525  hashennn  10526  hashunlem  10550  hashprg  10554  fihashssdif  10564  zfz1isolem1  10583  shftlem  10588  shftfvalg  10590  shftfval  10593  replim  10631  cjexp  10665  resqrexlemcalc1  10786  resqrexlemcvg  10791  rersqrtthlem  10802  abssq  10853  recan  10881  negfi  10999  minclpr  11008  xrmaxiflemcom  11018  xrmineqinf  11038  xrminltinf  11041  xrminadd  11044  climmpt  11069  climrecl  11093  fsum3cvg  11147  summodclem3  11149  summodclem2a  11150  modfsummodlemstep  11226  isumsplit  11260  arisum  11267  geosergap  11275  geo2sum  11283  mertenslemi1  11304  mertenslem2  11305  clim2divap  11309  fproddccvg  11341  efcj  11379  efsub  11387  eflegeo  11408  sinneg  11433  cosneg  11434  sin01bnd  11464  cos01bnd  11465  summodnegmod  11524  dvdseq  11546  addmodlteqALT  11557  mulmoddvds  11561  zob  11588  nn0ob  11605  divalgmod  11624  flodddiv4  11631  divgcdnnr  11664  gcdneg  11670  bezoutlemsup  11697  dvdssq  11719  lcmneg  11755  3lcm2e6woprm  11767  6lcm4e12  11768  divgcdcoprmex  11783  cncongr1  11784  cncongrcoprm  11787  oddpwdclemxy  11847  oddpwdclemodd  11850  divnumden  11874  zgcdsq  11879  phibnd  11893  hashgcdlem  11903  ennnfonelemex  11927  strndxid  11987  topnvalg  12132  toponcom  12194  tgtopon  12235  restopnb  12350  cnptoprest  12408  blfvalps  12554  bdmopn  12673  cnmet  12699  limcdifap  12800  dviaddf  12838  dvexp  12844  coseq0negpitopi  12917  abssinper  12927  subctctexmid  13196  cvgcmp2nlemabs  13227  trilpolemlt1  13234