Theorem eqcomd 2202

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 2198	. 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 1461  ax-gen 1463  ax-ext 2178

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

This theorem is referenced by:  eqtr2d  2230  eqtr3d  2231  eqtr4d  2232  eqtr2id  2242  eqtr2di  2246  sylan9req  2250  eqeltrrd  2274  eleqtrrd  2276  eleqtrrid  2286  eqeltrrdi  2288  eqnetrrd  2393  neeqtrrd  2397  rspcedeq2vd  2878  dedhb  2933  eqsstrrd  3221  sseqtrrd  3223  eqsstrrdi  3237  dfrab3ss  3442  uneqdifeqim  3537  ifbothdadc  3594  ifbothdc  3595  disjsn2  3686  diftpsn3  3764  dfopg  3807  unimax  3874  sndisj  4030  eqbrtrrd  4058  breqtrrd  4062  breqtrrid  4072  eqbrtrrdi  4074  class2seteq  4197  opth1  4270  euotd  4288  opelopabsb  4295  tfisi  4624  0nelxp  4692  opeliunxp  4719  euiotaex  5236  iota4  5239  iotam  5251  fun2ssres  5302  funimass1  5336  funssfv  5587  fnimapr  5624  fvun1  5630  fvco4  5636  elfvmptrab  5660  fmptco  5731  foima2  5801  foeqcnvco  5840  f1eqcocnv  5841  f1oiso2  5877  riotass2  5907  riotass  5908  f1ocnvfv3  5914  fvmpopr2d  6063  caovlem2d  6120  f1opw2  6133  offveq  6160  sbcopeq1a  6254  csbopeq1a  6255  eloprabi  6263  cnvf1olem  6291  f2ndf  6293  smoiso  6369  nnaword  6578  eqer  6633  uniqs  6661  mapsncnv  6763  ixpiinm  6792  mapsnf1o  6805  ssenen  6921  findcard2  6959  findcard2s  6960  unsnfidcex  6990  fisseneq  7004  phpeqd  7005  en1eqsn  7023  sbthlemi6  7037  updjud  7157  omp1eomlem  7169  nnnninf2  7202  nninfisollem0  7205  nninfisollemeq  7207  fodju0  7222  3nsssucpw1  7321  enq0sym  7518  enq0tr  7520  recexgt0sr  7859  caucvgsrlemoffcau  7884  axcaucvglemval  7983  le2tri3i  8154  cnegexlem2  8221  nnpcan  8268  addlsub  8415  negf1o  8427  subdi  8430  rereim  8632  cru  8648  divmulassap  8741  divmulasscomap  8742  divap1d  8847  subhalfhalf  9245  div4p1lem1div2  9264  difgtsumgt  9414  elz2  9416  zindd  9463  qapne  9732  divge1  9817  xrlttri3  9891  fseq1p1m1  10188  fzrevral  10199  nn0disj  10232  fzosplitsnm1  10304  fzosplitprm1  10329  flqlelt  10385  divfl0  10405  flqpmodeq  10438  zmodidfzo  10464  modqmuladd  10477  qnegmod  10480  addmodid  10483  modifeq2int  10497  modqeqmodmin  10505  modfzo0difsn  10506  modsumfzodifsn  10507  addmodlteq  10509  frecuzrdgsuc  10525  frecfzen2  10538  iseqf1olemab  10613  iseqf1olemmo  10616  seqf1oglem1  10630  seqf1oglem2  10631  ser3sub  10634  expgt1  10688  leexp2r  10704  sqoddm1div8  10804  mulsubdivbinom2ap  10822  bcm1k  10871  bcn2m1  10880  hashinfuni  10888  hashennnuni  10890  hashennn  10891  hashunlem  10915  hashprg  10919  fihashssdif  10929  zfz1isolem1  10951  elovmpowrd  10995  shftlem  11000  shftfvalg  11002  shftfval  11005  replim  11043  cjexp  11077  resqrexlemcalc1  11198  resqrexlemcvg  11203  rersqrtthlem  11214  abssq  11265  recan  11293  negfi  11412  minclpr  11421  mingeb  11426  xrmaxiflemcom  11433  xrmineqinf  11453  xrminltinf  11456  xrminadd  11459  climmpt  11484  climrecl  11508  fsum3cvg  11562  summodclem3  11564  summodclem2a  11565  modfsummodlemstep  11641  isumsplit  11675  arisum  11682  geosergap  11690  geo2sum  11698  mertenslemi1  11719  mertenslem2  11720  clim2divap  11724  fproddccvg  11756  fprodssdc  11774  fprodabs  11800  fproddivapf  11815  fprodmodd  11825  efcj  11857  efsub  11865  eflegeo  11885  sinneg  11910  cosneg  11911  sin01bnd  11941  cos01bnd  11942  modm1div  11984  summodnegmod  12006  dvdseq  12032  addmodlteqALT  12043  mulmoddvds  12047  zob  12075  nn0ob  12092  divalgmod  12111  flodddiv4  12120  bitsinv1  12146  divgcdnnr  12170  gcdneg  12176  bezoutlemsup  12203  dvdssq  12225  lcmneg  12269  3lcm2e6woprm  12281  6lcm4e12  12282  divgcdcoprmex  12297  cncongr1  12298  cncongrcoprm  12301  oddpwdclemxy  12364  oddpwdclemodd  12367  divnumden  12391  zgcdsq  12396  phibnd  12412  hashgcdlem  12433  vfermltl  12447  powm2modprm  12448  reumodprminv  12449  pythagtriplem19  12478  pcprendvds2  12487  pczpre  12493  dvdsprmpweqle  12533  difsqpwdvds  12534  4sqlem4  12588  ennnfonelemex  12658  strndxid  12733  topnvalg  12955  prdssca  12979  intopsn  13071  ismgmid2  13084  mgmidsssn0  13088  gsumfzval  13095  gsumprval  13103  mndpfo  13142  mndfo  13143  mndinvmod  13149  prds0g  13153  mnd1id  13160  mhmf1o  13174  0mhm  13190  gsumwmhm  13202  grpidd2  13245  grpinvid2  13257  grpidssd  13280  grpnpcan  13296  grpsubsub4  13297  qusgrp2  13321  mulginvcom  13355  grpissubg  13402  quselbasg  13438  qus0  13443  ecqusaddd  13446  ghmid  13457  ghminv  13458  imasabl  13544  gsumfzmhm  13551  mgpress  13565  rnglz  13579  rngrz  13580  rngmneg1  13581  rngmneg2  13582  rngpropd  13589  srg1zr  13621  srgmulgass  13623  srgpcomp  13624  srgpcomppsc  13626  ringadd2  13661  ringo2times  13662  ringlz  13677  ringrz  13678  ringinvnzdiv  13684  ringnegl  13685  ringnegr  13686  imasring  13698  qusring2  13700  crngunit  13745  rhmopp  13810  lringuplu  13830  opprdomnbg  13908  lmod0vs  13955  lmodvsmmulgdi  13957  lmodfopne  13960  islss3  14013  lspsn  14050  lmodindp1  14062  rnglidlmmgm  14130  rnglidlmsgrp  14131  rnglidlrng  14132  isridl  14138  zringinvg  14238  zndvds  14283  znf1o  14285  psrgrp  14315  toponcom  14349  tgtopon  14388  restopnb  14503  cnptoprest  14561  blfvalps  14707  bdmopn  14826  cnmet  14852  mpomulcn  14888  limcdifap  14984  dvidsslem  15015  dviaddf  15027  dvexp  15033  dvply2g  15088  coseq0negpitopi  15158  abssinper  15168  rplogbzexp  15276  dvdsppwf1o  15311  mpodvdsmulf1o  15312  fsumdvdsmul  15313  sgmmul  15318  perfect  15323  lgsvalmod  15346  lgsneg  15351  gausslemma2dlem1a  15385  gausslemma2dlem6  15394  gausslemma2dlem7  15395  gausslemma2d  15396  lgsquadlem2  15405  2lgslem1a1  15413  2lgslem1a  15415  2lgslem3c  15422  2lgslem3d  15423  2lgslem3d1  15427  2lgs  15431  2lgsoddprm  15440  subctctexmid  15733  cvgcmp2nlemabs  15767  trilpolemlt1  15776