Theorem eqcomd 2160

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

Syntax hints:   → wi 4   = wceq 1332

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 1424  ax-gen 1426  ax-ext 2136

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

This theorem is referenced by:  eqtr2d  2188  eqtr3d  2189  eqtr4d  2190  syl5req  2200  eqtr2di  2204  sylan9req  2208  eqeltrrd  2232  eleqtrrd  2234  eleqtrrid  2244  eqeltrrdi  2246  eqnetrrd  2350  neeqtrrd  2354  rspcedeq2vd  2823  dedhb  2877  eqsstrrd  3161  sseqtrrd  3163  eqsstrrdi  3177  dfrab3ss  3381  uneqdifeqim  3475  ifbothdadc  3532  ifbothdc  3533  disjsn2  3618  diftpsn3  3693  dfopg  3735  unimax  3802  sndisj  3957  eqbrtrrd  3984  breqtrrd  3988  breqtrrid  3998  eqbrtrrdi  4000  class2seteq  4119  opth1  4191  euotd  4209  opelopabsb  4215  tfisi  4540  0nelxp  4607  opeliunxp  4634  euiotaex  5144  iota4  5146  fun2ssres  5206  funimass1  5240  funssfv  5487  fnimapr  5521  fvun1  5527  fvco4  5533  elfvmptrab  5556  fmptco  5626  foima2  5693  foeqcnvco  5731  f1eqcocnv  5732  f1oiso2  5768  riotass2  5796  riotass  5797  f1ocnvfv3  5803  caovlem2d  6003  f1opw2  6016  sbcopeq1a  6125  csbopeq1a  6126  eloprabi  6134  cnvf1olem  6161  f2ndf  6163  smoiso  6239  nnaword  6447  eqer  6501  uniqs  6527  mapsncnv  6629  ixpiinm  6658  mapsnf1o  6671  ssenen  6785  findcard2  6823  findcard2s  6824  unsnfidcex  6853  fisseneq  6865  phpeqd  6866  en1eqsn  6881  sbthlemi6  6895  updjud  7012  omp1eomlem  7024  nnnninf2  7055  fodju0  7069  3nsssucpw1  7150  enq0sym  7331  enq0tr  7333  recexgt0sr  7672  caucvgsrlemoffcau  7697  axcaucvglemval  7796  le2tri3i  7964  cnegexlem2  8030  nnpcan  8077  addlsub  8224  negf1o  8236  subdi  8239  rereim  8440  cru  8456  divmulassap  8547  divmulasscomap  8548  divap1d  8653  div4p1lem1div2  9065  elz2  9214  zindd  9261  qapne  9526  divge1  9608  xrlttri3  9682  fseq1p1m1  9974  fzrevral  9985  nn0disj  10015  fzosplitsnm1  10086  fzosplitprm1  10111  flqlelt  10153  divfl0  10173  flqpmodeq  10204  zmodidfzo  10230  modqmuladd  10243  qnegmod  10246  addmodid  10249  modifeq2int  10263  modqeqmodmin  10271  modfzo0difsn  10272  modsumfzodifsn  10273  addmodlteq  10275  frecuzrdgsuc  10291  frecfzen2  10304  iseqf1olemab  10366  iseqf1olemmo  10369  ser3sub  10383  expgt1  10435  leexp2r  10451  sqoddm1div8  10548  bcm1k  10611  bcn2m1  10620  hashinfuni  10628  hashennnuni  10630  hashennn  10631  hashunlem  10655  hashprg  10659  fihashssdif  10669  zfz1isolem1  10688  shftlem  10693  shftfvalg  10695  shftfval  10698  replim  10736  cjexp  10770  resqrexlemcalc1  10891  resqrexlemcvg  10896  rersqrtthlem  10907  abssq  10958  recan  10986  negfi  11104  minclpr  11113  xrmaxiflemcom  11123  xrmineqinf  11143  xrminltinf  11146  xrminadd  11149  climmpt  11174  climrecl  11198  fsum3cvg  11252  summodclem3  11254  summodclem2a  11255  modfsummodlemstep  11331  isumsplit  11365  arisum  11372  geosergap  11380  geo2sum  11388  mertenslemi1  11409  mertenslem2  11410  clim2divap  11414  fproddccvg  11446  fprodssdc  11464  fprodabs  11490  fproddivapf  11505  fprodmodd  11515  efcj  11547  efsub  11555  eflegeo  11575  sinneg  11600  cosneg  11601  sin01bnd  11631  cos01bnd  11632  summodnegmod  11691  dvdseq  11713  addmodlteqALT  11724  mulmoddvds  11728  zob  11755  nn0ob  11772  divalgmod  11791  flodddiv4  11798  divgcdnnr  11831  gcdneg  11837  bezoutlemsup  11864  dvdssq  11886  lcmneg  11922  3lcm2e6woprm  11934  6lcm4e12  11935  divgcdcoprmex  11950  cncongr1  11951  cncongrcoprm  11954  oddpwdclemxy  12014  oddpwdclemodd  12017  divnumden  12041  zgcdsq  12046  phibnd  12060  hashgcdlem  12070  ennnfonelemex  12094  strndxid  12157  topnvalg  12302  toponcom  12364  tgtopon  12405  restopnb  12520  cnptoprest  12578  blfvalps  12724  bdmopn  12843  cnmet  12869  limcdifap  12970  dviaddf  13008  dvexp  13014  coseq0negpitopi  13096  abssinper  13106  rplogbzexp  13210  subctctexmid  13512  cvgcmp2nlemabs  13544  trilpolemlt1  13553