Theorem eqcomd 2237

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-ext 2213

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

This theorem is referenced by:  eqtr2d  2265  eqtr3d  2266  eqtr4d  2267  eqtr2id  2277  eqtr2di  2281  sylan9req  2285  eqeltrrd  2309  eleqtrrd  2311  eleqtrrid  2321  eqeltrrdi  2323  eqnetrrd  2428  neeqtrrd  2432  rspcedeq2vd  2920  dedhb  2975  eqsstrrd  3264  sseqtrrd  3266  eqsstrrdi  3280  dfrab3ss  3485  uneqdifeqim  3580  ifbothdadc  3639  ifbothdc  3640  2if2dc  3645  disjsn2  3732  diftpsn3  3814  elpr2elpr  3859  dfopg  3860  unimax  3927  sndisj  4084  eqbrtrrd  4112  breqtrrd  4116  breqtrrid  4126  eqbrtrrdi  4128  class2seteq  4253  opth1  4328  euotd  4347  opelopabsb  4354  tfisi  4685  0nelxp  4753  opeliunxp  4781  euiotaex  5303  iota4  5306  iotam  5318  fun2ssres  5370  funimass1  5407  funssfv  5665  fnimapr  5706  fvun1  5712  fvco4  5718  elfvmptrab  5742  fmptco  5813  fncofn  5832  foima2  5892  foeqcnvco  5931  f1eqcocnv  5932  f1oiso2  5968  riotass2  6000  riotass  6001  f1ocnvfv3  6007  fvmpopr2d  6158  caovlem2d  6215  f1opw2  6229  offveq  6256  sbcopeq1a  6350  csbopeq1a  6351  eloprabi  6361  cnvf1olem  6389  f2ndf  6391  smoiso  6468  nnaword  6679  eqer  6734  uniqs  6762  mapsncnv  6864  ixpiinm  6893  mapsnf1o  6906  ssenen  7037  findcard2  7078  findcard2s  7079  unsnfidcex  7112  fisseneq  7127  phpeqd  7128  en1eqsn  7147  sbthlemi6  7161  updjud  7281  omp1eomlem  7293  nnnninf2  7326  nninfisollem0  7329  nninfisollemeq  7331  fodju0  7346  3nsssucpw1  7454  enq0sym  7652  enq0tr  7654  recexgt0sr  7993  caucvgsrlemoffcau  8018  axcaucvglemval  8117  le2tri3i  8288  cnegexlem2  8355  nnpcan  8402  addlsub  8549  negf1o  8561  subdi  8564  rereim  8766  cru  8782  divmulassap  8875  divmulasscomap  8876  divap1d  8981  subhalfhalf  9379  div4p1lem1div2  9398  difgtsumgt  9549  elz2  9551  zindd  9598  qapne  9873  divge1  9958  xrlttri3  10032  fseq1p1m1  10329  fzrevral  10340  nn0disj  10373  fzo0addel  10434  fzosplitsnm1  10455  fzosplitprm1  10481  flqlelt  10537  divfl0  10557  flqpmodeq  10590  zmodidfzo  10616  modqmuladd  10629  qnegmod  10632  addmodid  10635  modifeq2int  10649  modqeqmodmin  10657  modfzo0difsn  10658  modsumfzodifsn  10659  addmodlteq  10661  frecuzrdgsuc  10677  frecfzen2  10690  iseqf1olemab  10765  iseqf1olemmo  10768  seqf1oglem1  10782  seqf1oglem2  10783  ser3sub  10786  expgt1  10840  leexp2r  10856  sqoddm1div8  10956  mulsubdivbinom2ap  10974  bcm1k  11023  bcn2m1  11032  hashinfuni  11040  hashennnuni  11042  hashennn  11043  hashunlem  11068  hashprg  11073  fihashssdif  11083  zfz1isolem1  11105  elovmpowrd  11156  ccatsymb  11180  ccatlid  11184  eqs1  11206  ccatw2s1p1g  11223  swrdfv2  11245  swrds1  11250  swrdlsw  11251  pfxfv  11266  swrdswrd  11287  swrdpfx  11289  pfxpfx  11290  pfxlswccat  11295  ccats1pfxeq  11296  wrdind  11304  wrd2ind  11305  pfxccatin12lem1  11310  pfxccatin12lem2  11313  swrdccat3blem  11321  swrdccat3b  11322  ccats1pfxeqbi  11324  reuccatpfxs1lem  11328  reuccatpfxs1  11329  shftlem  11378  shftfvalg  11380  shftfval  11383  replim  11421  cjexp  11455  resqrexlemcalc1  11576  resqrexlemcvg  11581  rersqrtthlem  11592  abssq  11643  recan  11671  negfi  11790  minclpr  11799  mingeb  11804  xrmaxiflemcom  11811  xrmineqinf  11831  xrminltinf  11834  xrminadd  11837  climmpt  11862  climrecl  11886  fsum3cvg  11941  summodclem3  11943  summodclem2a  11944  modfsummodlemstep  12020  isumsplit  12054  arisum  12061  geosergap  12069  geo2sum  12077  mertenslemi1  12098  mertenslem2  12099  clim2divap  12103  fproddccvg  12135  fprodssdc  12153  fprodabs  12179  fproddivapf  12194  fprodmodd  12204  efcj  12236  efsub  12244  eflegeo  12264  sinneg  12289  cosneg  12290  sin01bnd  12320  cos01bnd  12321  modm1div  12363  summodnegmod  12385  dvdseq  12411  addmodlteqALT  12422  mulmoddvds  12426  zob  12454  nn0ob  12471  divalgmod  12490  flodddiv4  12499  bitsinv1  12525  divgcdnnr  12549  gcdneg  12555  bezoutlemsup  12582  dvdssq  12604  lcmneg  12648  3lcm2e6woprm  12660  6lcm4e12  12661  divgcdcoprmex  12676  cncongr1  12677  cncongrcoprm  12680  oddpwdclemxy  12743  oddpwdclemodd  12746  divnumden  12770  zgcdsq  12775  phibnd  12791  hashgcdlem  12812  vfermltl  12826  powm2modprm  12827  reumodprminv  12828  pythagtriplem19  12857  pcprendvds2  12866  pczpre  12872  dvdsprmpweqle  12912  difsqpwdvds  12913  4sqlem4  12967  ennnfonelemex  13037  strndxid  13112  topnvalg  13336  prdssca  13360  intopsn  13452  ismgmid2  13465  mgmidsssn0  13469  gsumfzval  13476  gsumprval  13484  mndpfo  13523  mndfo  13524  mndinvmod  13530  prds0g  13534  mnd1id  13541  mhmf1o  13555  0mhm  13571  gsumwmhm  13583  grpidd2  13626  grpinvid2  13638  grpidssd  13661  grpnpcan  13677  grpsubsub4  13678  qusgrp2  13702  mulginvcom  13736  grpissubg  13783  quselbasg  13819  qus0  13824  ecqusaddd  13827  ghmid  13838  ghminv  13839  imasabl  13925  gsumfzmhm  13932  gsumsplit0  13935  mgpress  13947  rnglz  13961  rngrz  13962  rngmneg1  13963  rngmneg2  13964  rngpropd  13971  srg1zr  14003  srgmulgass  14005  srgpcomp  14006  srgpcomppsc  14008  ringadd2  14043  ringo2times  14044  ringlz  14059  ringrz  14060  ringinvnzdiv  14066  ringnegl  14067  ringnegr  14068  imasring  14080  qusring2  14082  crngunit  14128  rhmopp  14193  lringuplu  14213  opprdomnbg  14291  lmod0vs  14338  lmodvsmmulgdi  14340  lmodfopne  14343  islss3  14396  lspsn  14433  lmodindp1  14445  rnglidlmmgm  14513  rnglidlmsgrp  14514  rnglidlrng  14515  isridl  14521  zringinvg  14621  zndvds  14666  znf1o  14668  psrgrp  14702  toponcom  14754  tgtopon  14793  restopnb  14908  cnptoprest  14966  blfvalps  15112  bdmopn  15231  cnmet  15257  mpomulcn  15293  limcdifap  15389  dvidsslem  15420  dviaddf  15432  dvexp  15438  dvply2g  15493  coseq0negpitopi  15563  abssinper  15573  rplogbzexp  15681  dvdsppwf1o  15716  mpodvdsmulf1o  15717  fsumdvdsmul  15718  sgmmul  15723  perfect  15728  lgsvalmod  15751  lgsneg  15756  gausslemma2dlem1a  15790  gausslemma2dlem6  15799  gausslemma2dlem7  15800  gausslemma2d  15801  lgsquadlem2  15810  2lgslem1a1  15818  2lgslem1a  15820  2lgslem3c  15827  2lgslem3d  15828  2lgslem3d1  15832  2lgs  15836  2lgsoddprm  15845  uhgrun  15940  upgrun  15980  umgrun  15982  ushgredgedg  16080  issubgr2  16112  uhgrissubgr  16115  subgruhgredgdm  16124  subumgredg2en  16125  subupgr  16127  p1evtxdeqfilem  16165  wlklenvm1  16195  wlklenvm1g  16196  wlkl1loop  16212  upgriswlkdc  16214  uspgr2wlkeq  16219  uspgr2wlkeq2  16220  uspgr2wlkeqi  16221  wlkres  16233  loopclwwlkn1b  16273  clwwlkn1loopb  16274  clwwlkext2edg  16276  clwwlknonccat  16287  s2elclwwlknon2  16290  clwwlknonex2lem2  16292  clwwlknun  16295  eupth2lem3fi  16330  eupth2lembfi  16331  subctctexmid  16622  cvgcmp2nlemabs  16657  trilpolemlt1  16666  gsumgfsumlem  16704  gfsumsn  16706