Theorem eqcomd 2238

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-ext 2214

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

This theorem is referenced by:  eqtr2d  2266  eqtr3d  2267  eqtr4d  2268  eqtr2id  2278  eqtr2di  2282  sylan9req  2286  eqeltrrd  2310  eleqtrrd  2312  eleqtrrid  2322  eqeltrrdi  2324  eqabcdv  2364  eqnetrrd  2438  neeqtrrd  2442  rspcedeq2vd  2930  dedhb  2985  eqsstrrd  3274  sseqtrrd  3276  eqsstrrdi  3290  dfrab3ss  3498  uneqdifeqim  3594  ifbothdadc  3655  ifbothdc  3656  2if2dc  3661  disjsn2  3751  diftpsn3  3834  elpr2elpr  3879  dfopg  3880  unimax  3947  sndisj  4104  eqbrtrrd  4132  breqtrrd  4136  breqtrrid  4146  eqbrtrrdi  4148  class2seteq  4275  opth1  4351  euotd  4370  opelopabsb  4377  tfisi  4708  0nelxp  4776  opeliunxp  4804  euiotaex  5328  iota4  5331  iotam  5343  fun2ssres  5395  funimass1  5432  funssfv  5695  fnimapr  5736  fvun1  5742  fvco4  5748  elfvmptrab  5772  fmptco  5842  fncofn  5861  foima2  5923  foeqcnvco  5962  f1eqcocnv  5963  f1oiso2  5999  riotass2  6031  riotass  6032  f1ocnvfv3  6038  fvmpopr2d  6189  caovlem2d  6246  f1opw2  6260  offveq  6286  sbcopeq1a  6380  csbopeq1a  6381  eloprabi  6391  cnvf1olem  6419  f2ndf  6421  suppval1  6438  suppsnopdc  6449  smoiso  6532  nnaword  6743  eqer  6798  uniqs  6826  mapsncnv  6929  ixpiinm  6958  mapsnf1o  6971  mapunen  7103  ssenen  7104  findcard2  7145  findcard2s  7146  unsnfidcex  7179  fisseneq  7194  phpeqd  7195  en1eqsn  7217  sbthlemi6  7231  updjud  7372  omp1eomlem  7384  nnnninf2  7417  nninfisollem0  7420  nninfisollemeq  7422  fodju0  7437  3nsssucpw1  7545  enq0sym  7743  enq0tr  7745  recexgt0sr  8084  caucvgsrlemoffcau  8109  axcaucvglemval  8208  le2tri3i  8378  cnegexlem2  8445  nnpcan  8492  addlsub  8639  negf1o  8651  subdi  8654  rereim  8856  cru  8872  divmulassap  8965  divmulasscomap  8966  divap1d  9071  subhalfhalf  9469  div4p1lem1div2  9488  difgtsumgt  9643  elz2  9645  zindd  9692  qapne  9967  divge1  10052  xrlttri3  10126  fseq1p1m1  10424  fzrevral  10435  nn0disj  10468  fzo0addel  10529  fzosplitsnm1  10550  fzosplitprm1  10576  flqlelt  10632  divfl0  10652  flqpmodeq  10685  zmodidfzo  10711  modqmuladd  10724  qnegmod  10727  addmodid  10730  modifeq2int  10744  modqeqmodmin  10752  modfzo0difsn  10753  modsumfzodifsn  10754  addmodlteq  10756  frecuzrdgsuc  10772  frecfzen2  10785  iseqf1olemab  10860  iseqf1olemmo  10863  seqf1oglem1  10877  seqf1oglem2  10878  ser3sub  10881  expgt1  10935  leexp2r  10951  sqoddm1div8  11051  mulsubdivbinom2ap  11069  bcm1k  11118  bcn2m1  11127  hashinfuni  11135  hashennnuni  11137  hashennn  11138  hashunlem  11163  hashprg  11168  fihashssdif  11178  hashfibclem  11199  hashfibc  11200  zfz1isolem1  11205  elovmpowrd  11259  ccatsymb  11283  ccatlid  11287  eqs1  11309  ccatw2s1p1g  11326  swrdfv2  11348  swrds1  11353  swrdlsw  11354  pfxfv  11369  swrdswrd  11390  swrdpfx  11392  pfxpfx  11393  pfxlswccat  11398  ccats1pfxeq  11399  wrdind  11407  wrd2ind  11408  pfxccatin12lem1  11413  pfxccatin12lem2  11416  swrdccat3blem  11424  swrdccat3b  11425  ccats1pfxeqbi  11427  reuccatpfxs1lem  11431  reuccatpfxs1  11432  s3s4d  11488  s2s5d  11489  s5s2d  11490  shftlem  11494  shftfvalg  11496  shftfval  11499  replim  11537  cjexp  11571  resqrexlemcalc1  11692  resqrexlemcvg  11697  rersqrtthlem  11708  abssq  11759  recan  11787  negfi  11906  minclpr  11915  mingeb  11920  xrmaxiflemcom  11927  xrmineqinf  11947  xrminltinf  11950  xrminadd  11953  climmpt  11978  climrecl  12002  fsum3cvg  12057  summodclem3  12059  summodclem2a  12060  modfsummodlemstep  12136  isumsplit  12170  arisum  12177  geosergap  12185  geo2sum  12193  mertenslemi1  12214  mertenslem2  12215  clim2divap  12219  fproddccvg  12251  fprodssdc  12269  fprodabs  12295  fproddivapf  12310  fprodmodd  12320  efcj  12352  efsub  12360  eflegeo  12380  sinneg  12405  cosneg  12406  sin01bnd  12436  cos01bnd  12437  modm1div  12479  summodnegmod  12501  dvdseq  12527  addmodlteqALT  12538  mulmoddvds  12542  zob  12570  nn0ob  12587  divalgmod  12606  flodddiv4  12615  bitsinv1  12641  divgcdnnr  12665  gcdneg  12671  bezoutlemsup  12698  dvdssq  12720  lcmneg  12764  3lcm2e6woprm  12776  6lcm4e12  12777  divgcdcoprmex  12792  cncongr1  12793  cncongrcoprm  12796  oddpwdclemxy  12859  oddpwdclemodd  12862  divnumden  12886  zgcdsq  12891  phibnd  12907  hashgcdlem  12928  vfermltl  12942  powm2modprm  12943  reumodprminv  12944  pythagtriplem19  12973  pcprendvds2  12982  pczpre  12988  dvdsprmpweqle  13028  difsqpwdvds  13029  4sqlem4  13083  ennnfonelemex  13154  strndxid  13229  topnvalg  13453  prdssca  13477  intopsn  13569  ismgmid2  13582  mgmidsssn0  13586  gsumfzval  13593  gsumprval  13601  mndpfo  13640  mndfo  13641  mndinvmod  13647  prds0g  13651  mnd1id  13658  mhmf1o  13672  0mhm  13688  gsumwmhm  13700  grpidd2  13743  grpinvid2  13755  grpidssd  13778  grpnpcan  13794  grpsubsub4  13795  qusgrp2  13819  mulginvcom  13853  grpissubg  13900  quselbasg  13936  qus0  13941  ecqusaddd  13944  ghmid  13955  ghminv  13956  imasabl  14042  gsumfzmhm  14049  gsumsplit0  14052  mgpress  14064  rnglz  14078  rngrz  14079  rngmneg1  14080  rngmneg2  14081  rngpropd  14088  srg1zr  14120  srgmulgass  14122  srgpcomp  14123  srgpcomppsc  14125  ringadd2  14160  ringo2times  14161  ringlz  14176  ringrz  14177  ringinvnzdiv  14183  ringnegl  14184  ringnegr  14185  imasring  14197  qusring2  14199  crngunit  14245  rhmopp  14310  lringuplu  14330  opprdomnbg  14409  lmod0vs  14456  lmodvsmmulgdi  14458  lmodfopne  14461  islss3  14514  lspsn  14551  lmodindp1  14563  rnglidlmmgm  14631  rnglidlmsgrp  14632  rnglidlrng  14633  isridl  14639  zringinvg  14739  zndvds  14784  znf1o  14786  psrgrp  14827  toponcom  14879  tgtopon  14918  restopnb  15033  cnptoprest  15091  blfvalps  15237  bdmopn  15356  cnmet  15382  mpomulcn  15418  limcdifap  15514  dvidsslem  15545  dviaddf  15557  dvexp  15563  dvply2g  15618  coseq0negpitopi  15688  abssinper  15698  rplogbzexp  15806  pellexlem2  15833  dvdsppwf1o  15844  mpodvdsmulf1o  15845  fsumdvdsmul  15846  sgmmul  15851  perfect  15856  lgsvalmod  15879  lgsneg  15884  gausslemma2dlem1a  15918  gausslemma2dlem6  15927  gausslemma2dlem7  15928  gausslemma2d  15929  lgsquadlem2  15938  2lgslem1a1  15946  2lgslem1a  15948  2lgslem3c  15955  2lgslem3d  15956  2lgslem3d1  15960  2lgs  15964  2lgsoddprm  15973  uhgrun  16068  upgrun  16108  umgrun  16110  ushgredgedg  16208  issubgr2  16240  uhgrissubgr  16243  subgruhgredgdm  16252  subumgredg2en  16253  subupgr  16255  p1evtxdeqfilem  16293  wlklenvm1  16323  wlklenvm1g  16324  wlkl1loop  16340  upgriswlkdc  16342  uspgr2wlkeq  16347  uspgr2wlkeq2  16348  uspgr2wlkeqi  16349  wlkres  16361  loopclwwlkn1b  16401  clwwlkn1loopb  16402  clwwlkext2edg  16404  clwwlknonccat  16415  s2elclwwlknon2  16418  clwwlknonex2lem2  16420  clwwlknun  16423  eupth2lem3fi  16458  eupth2lembfi  16459  subctctexmid  16761  cvgcmp2nlemabs  16803  trilpolemlt1  16812  gsumgfsumlem  16851  gfsumsn  16853