Theorem eqcomd 2212

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-ext 2188

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

This theorem is referenced by:  eqtr2d  2240  eqtr3d  2241  eqtr4d  2242  eqtr2id  2252  eqtr2di  2256  sylan9req  2260  eqeltrrd  2284  eleqtrrd  2286  eleqtrrid  2296  eqeltrrdi  2298  eqnetrrd  2403  neeqtrrd  2407  rspcedeq2vd  2888  dedhb  2943  eqsstrrd  3231  sseqtrrd  3233  eqsstrrdi  3247  dfrab3ss  3452  uneqdifeqim  3547  ifbothdadc  3605  ifbothdc  3606  disjsn2  3697  diftpsn3  3776  dfopg  3819  unimax  3886  sndisj  4043  eqbrtrrd  4071  breqtrrd  4075  breqtrrid  4085  eqbrtrrdi  4087  class2seteq  4211  opth1  4284  euotd  4303  opelopabsb  4310  tfisi  4639  0nelxp  4707  opeliunxp  4734  euiotaex  5253  iota4  5256  iotam  5268  fun2ssres  5319  funimass1  5356  funssfv  5609  fnimapr  5646  fvun1  5652  fvco4  5658  elfvmptrab  5682  fmptco  5753  foima2  5827  foeqcnvco  5866  f1eqcocnv  5867  f1oiso2  5903  riotass2  5933  riotass  5934  f1ocnvfv3  5940  fvmpopr2d  6089  caovlem2d  6146  f1opw2  6159  offveq  6186  sbcopeq1a  6280  csbopeq1a  6281  eloprabi  6289  cnvf1olem  6317  f2ndf  6319  smoiso  6395  nnaword  6604  eqer  6659  uniqs  6687  mapsncnv  6789  ixpiinm  6818  mapsnf1o  6831  ssenen  6955  findcard2  6993  findcard2s  6994  unsnfidcex  7024  fisseneq  7038  phpeqd  7039  en1eqsn  7057  sbthlemi6  7071  updjud  7191  omp1eomlem  7203  nnnninf2  7236  nninfisollem0  7239  nninfisollemeq  7241  fodju0  7256  3nsssucpw1  7355  enq0sym  7552  enq0tr  7554  recexgt0sr  7893  caucvgsrlemoffcau  7918  axcaucvglemval  8017  le2tri3i  8188  cnegexlem2  8255  nnpcan  8302  addlsub  8449  negf1o  8461  subdi  8464  rereim  8666  cru  8682  divmulassap  8775  divmulasscomap  8776  divap1d  8881  subhalfhalf  9279  div4p1lem1div2  9298  difgtsumgt  9449  elz2  9451  zindd  9498  qapne  9767  divge1  9852  xrlttri3  9926  fseq1p1m1  10223  fzrevral  10234  nn0disj  10267  fzo0addel  10324  fzosplitsnm1  10345  fzosplitprm1  10370  flqlelt  10426  divfl0  10446  flqpmodeq  10479  zmodidfzo  10505  modqmuladd  10518  qnegmod  10521  addmodid  10524  modifeq2int  10538  modqeqmodmin  10546  modfzo0difsn  10547  modsumfzodifsn  10548  addmodlteq  10550  frecuzrdgsuc  10566  frecfzen2  10579  iseqf1olemab  10654  iseqf1olemmo  10657  seqf1oglem1  10671  seqf1oglem2  10672  ser3sub  10675  expgt1  10729  leexp2r  10745  sqoddm1div8  10845  mulsubdivbinom2ap  10863  bcm1k  10912  bcn2m1  10921  hashinfuni  10929  hashennnuni  10931  hashennn  10932  hashunlem  10956  hashprg  10960  fihashssdif  10970  zfz1isolem1  10992  elovmpowrd  11042  ccatsymb  11066  ccatlid  11070  eqs1  11090  swrdfv2  11124  swrds1  11129  swrdlsw  11130  pfxfv  11143  swrdswrd  11164  swrdpfx  11166  pfxpfx  11167  shftlem  11171  shftfvalg  11173  shftfval  11176  replim  11214  cjexp  11248  resqrexlemcalc1  11369  resqrexlemcvg  11374  rersqrtthlem  11385  abssq  11436  recan  11464  negfi  11583  minclpr  11592  mingeb  11597  xrmaxiflemcom  11604  xrmineqinf  11624  xrminltinf  11627  xrminadd  11630  climmpt  11655  climrecl  11679  fsum3cvg  11733  summodclem3  11735  summodclem2a  11736  modfsummodlemstep  11812  isumsplit  11846  arisum  11853  geosergap  11861  geo2sum  11869  mertenslemi1  11890  mertenslem2  11891  clim2divap  11895  fproddccvg  11927  fprodssdc  11945  fprodabs  11971  fproddivapf  11986  fprodmodd  11996  efcj  12028  efsub  12036  eflegeo  12056  sinneg  12081  cosneg  12082  sin01bnd  12112  cos01bnd  12113  modm1div  12155  summodnegmod  12177  dvdseq  12203  addmodlteqALT  12214  mulmoddvds  12218  zob  12246  nn0ob  12263  divalgmod  12282  flodddiv4  12291  bitsinv1  12317  divgcdnnr  12341  gcdneg  12347  bezoutlemsup  12374  dvdssq  12396  lcmneg  12440  3lcm2e6woprm  12452  6lcm4e12  12453  divgcdcoprmex  12468  cncongr1  12469  cncongrcoprm  12472  oddpwdclemxy  12535  oddpwdclemodd  12538  divnumden  12562  zgcdsq  12567  phibnd  12583  hashgcdlem  12604  vfermltl  12618  powm2modprm  12619  reumodprminv  12620  pythagtriplem19  12649  pcprendvds2  12658  pczpre  12664  dvdsprmpweqle  12704  difsqpwdvds  12705  4sqlem4  12759  ennnfonelemex  12829  strndxid  12904  topnvalg  13127  prdssca  13151  intopsn  13243  ismgmid2  13256  mgmidsssn0  13260  gsumfzval  13267  gsumprval  13275  mndpfo  13314  mndfo  13315  mndinvmod  13321  prds0g  13325  mnd1id  13332  mhmf1o  13346  0mhm  13362  gsumwmhm  13374  grpidd2  13417  grpinvid2  13429  grpidssd  13452  grpnpcan  13468  grpsubsub4  13469  qusgrp2  13493  mulginvcom  13527  grpissubg  13574  quselbasg  13610  qus0  13615  ecqusaddd  13618  ghmid  13629  ghminv  13630  imasabl  13716  gsumfzmhm  13723  mgpress  13737  rnglz  13751  rngrz  13752  rngmneg1  13753  rngmneg2  13754  rngpropd  13761  srg1zr  13793  srgmulgass  13795  srgpcomp  13796  srgpcomppsc  13798  ringadd2  13833  ringo2times  13834  ringlz  13849  ringrz  13850  ringinvnzdiv  13856  ringnegl  13857  ringnegr  13858  imasring  13870  qusring2  13872  crngunit  13917  rhmopp  13982  lringuplu  14002  opprdomnbg  14080  lmod0vs  14127  lmodvsmmulgdi  14129  lmodfopne  14132  islss3  14185  lspsn  14222  lmodindp1  14234  rnglidlmmgm  14302  rnglidlmsgrp  14303  rnglidlrng  14304  isridl  14310  zringinvg  14410  zndvds  14455  znf1o  14457  psrgrp  14491  toponcom  14543  tgtopon  14582  restopnb  14697  cnptoprest  14755  blfvalps  14901  bdmopn  15020  cnmet  15046  mpomulcn  15082  limcdifap  15178  dvidsslem  15209  dviaddf  15221  dvexp  15227  dvply2g  15282  coseq0negpitopi  15352  abssinper  15362  rplogbzexp  15470  dvdsppwf1o  15505  mpodvdsmulf1o  15506  fsumdvdsmul  15507  sgmmul  15512  perfect  15517  lgsvalmod  15540  lgsneg  15545  gausslemma2dlem1a  15579  gausslemma2dlem6  15588  gausslemma2dlem7  15589  gausslemma2d  15590  lgsquadlem2  15599  2lgslem1a1  15607  2lgslem1a  15609  2lgslem3c  15616  2lgslem3d  15617  2lgslem3d1  15621  2lgs  15625  2lgsoddprm  15634  uhgrun  15726  subctctexmid  16011  cvgcmp2nlemabs  16045  trilpolemlt1  16054