Theorem eqcomd 2240

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 2236	. 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 2216

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

This theorem is referenced by:  eqtr2d  2268  eqtr3d  2269  eqtr4d  2270  eqtr2id  2280  eqtr2di  2284  sylan9req  2288  eqeltrrd  2312  eleqtrrd  2314  eleqtrrid  2324  eqeltrrdi  2326  eqabcdv  2366  eqnetrrd  2440  neeqtrrd  2444  rspcedeq2vd  2934  dedhb  2989  eqsstrrd  3279  sseqtrrd  3281  eqsstrrdi  3295  dfrab3ss  3503  uneqdifeqim  3599  ifbothdadc  3660  ifbothdc  3661  2if2dc  3666  ifeqeqxdc  3673  disjsn2  3757  diftpsn3  3840  elpr2elpr  3885  dfopg  3886  unimax  3953  sndisj  4110  eqbrtrrd  4138  breqtrrd  4142  breqtrrid  4152  eqbrtrrdi  4154  class2seteq  4281  opth1  4357  euotd  4376  opelopabsb  4383  tfisi  4714  0nelxp  4782  opeliunxp  4810  euiotaex  5334  iota4  5337  iotam  5349  fun2ssres  5401  funimass1  5438  funssfv  5701  fnimapr  5742  fvun1  5748  fvco4  5754  elfvmptrab  5778  fmptco  5848  fncofn  5867  foima2  5930  foeqcnvco  5969  f1eqcocnv  5970  f1oiso2  6006  riotass2  6040  riotass  6041  f1ocnvfv3  6047  fvmpopr2d  6198  caovlem2d  6255  f1opw2  6269  offveq  6296  sbcopeq1a  6394  csbopeq1a  6395  eloprabi  6405  cnvf1olem  6433  f2ndf  6435  suppval1  6452  suppsnopdc  6463  smoiso  6546  nnaword  6757  eqer  6812  uniqs  6840  mapsncnv  6943  ixpiinm  6972  mapsnf1o  6985  mapunen  7117  ssenen  7118  findcard2  7159  findcard2s  7160  unsnfidcex  7193  fisseneq  7208  phpeqd  7209  en1eqsn  7231  sbthlemi6  7245  updjud  7386  omp1eomlem  7398  nnnninf2  7431  nninfisollem0  7434  nninfisollemeq  7436  fodju0  7451  3nsssucpw1  7559  enq0sym  7763  enq0tr  7765  recexgt0sr  8104  caucvgsrlemoffcau  8129  axcaucvglemval  8228  le2tri3i  8398  cnegexlem2  8466  nnpcan  8513  addlsub  8660  negf1o  8673  subdi  8676  rereim  8878  cru  8894  divmulassap  8989  divmulasscomap  8990  divap1d  9095  subhalfhalf  9493  div4p1lem1div2  9512  difgtsumgt  9667  elz2  9669  zindd  9717  qapne  9992  divge1  10077  xrlttri3  10152  fseq1p1m1  10453  fzrevral  10464  nn0disj  10497  fzo0addel  10558  fzosplitsnm1  10579  fzosplitprm1  10605  flqlelt  10663  divfl0  10683  flqpmodeq  10716  zmodidfzo  10742  modqmuladd  10755  qnegmod  10758  addmodid  10761  modifeq2int  10775  modqeqmodmin  10783  modfzo0difsn  10784  modsumfzodifsn  10785  addmodlteq  10787  frecuzrdgsuc  10803  frecfzen2  10816  iseqf1olemab  10891  iseqf1olemmo  10894  seqf1oglem1  10908  seqf1oglem2  10909  ser3sub  10912  expgt1  10966  leexp2r  10982  sqoddm1div8  11083  mulsubdivbinom2ap  11101  bcm1k  11150  bcn2m1  11160  hashinfuni  11168  hashennnuni  11170  hashennn  11171  hashunlem  11196  hashprg  11201  fihashssdif  11211  hashfibclem  11234  hashfibc  11235  zfz1isolem1  11240  elovmpowrd  11294  ccatsymb  11318  ccatlid  11322  eqs1  11344  ccatw2s1p1g  11361  swrdfv2  11383  swrds1  11388  swrdlsw  11389  pfxfv  11404  swrdswrd  11425  swrdpfx  11427  pfxpfx  11428  pfxlswccat  11433  ccats1pfxeq  11434  wrdind  11442  wrd2ind  11443  pfxccatin12lem1  11448  pfxccatin12lem2  11451  swrdccat3blem  11459  swrdccat3b  11460  ccats1pfxeqbi  11462  reuccatpfxs1lem  11466  reuccatpfxs1  11467  s3s4d  11523  s2s5d  11524  s5s2d  11525  shftlem  11529  shftfvalg  11531  shftfval  11534  replim  11572  cjexp  11606  resqrexlemcalc1  11727  resqrexlemcvg  11732  rersqrtthlem  11743  abssq  11794  recan  11822  negfi  11941  minclpr  11950  mingeb  11955  xrmaxiflemcom  11962  xrmineqinf  11982  xrminltinf  11985  xrminadd  11988  climmpt  12013  climrecl  12037  fsum3cvg  12092  summodclem3  12094  summodclem2a  12095  modfsummodlemstep  12171  isumsplit  12205  arisum  12212  geosergap  12220  geo2sum  12228  mertenslemi1  12249  mertenslem2  12250  clim2divap  12254  fproddccvg  12286  fprodssdc  12304  fprodabs  12330  fproddivapf  12345  fprodmodd  12355  efcj  12387  efsub  12395  eflegeo  12415  sinneg  12440  cosneg  12441  sin01bnd  12471  cos01bnd  12472  modm1div  12514  summodnegmod  12536  dvdseq  12562  addmodlteqALT  12573  mulmoddvds  12577  zob  12605  nn0ob  12622  divalgmod  12641  flodddiv4  12650  bitsinv1  12676  divgcdnnr  12700  gcdneg  12706  bezoutlemsup  12733  dvdssq  12755  lcmneg  12799  3lcm2e6woprm  12811  6lcm4e12  12812  divgcdcoprmex  12827  cncongr1  12828  cncongrcoprm  12831  oddpwdclemxy  12894  oddpwdclemodd  12897  divnumden  12921  zgcdsq  12926  phibnd  12942  hashgcdlem  12963  vfermltl  12977  powm2modprm  12978  reumodprminv  12979  pythagtriplem19  13008  pcprendvds2  13017  pczpre  13023  dvdsprmpweqle  13063  difsqpwdvds  13064  4sqlem4  13118  ballotfilemfp1  13178  ballotfilemsf1o  13204  ballotfilemrinv0  13223  ennnfonelemex  13252  strndxid  13327  topnvalg  13551  intopsn  13633  ismgmid2  13646  mgmidsssn0  13650  gsumfzval  13657  gsumprval  13665  mndpfo  13702  mndfo  13703  mndinvmod  13709  mnd1id  13714  mhmf1o  13728  0mhm  13744  gsumwmhm  13756  grpidd2  13799  grpinvid2  13811  grpidssd  13834  grpnpcan  13850  grpsubsub4  13851  qusgrp2  13869  mulginvcom  13903  grpissubg  13950  quselbasg  13986  qus0  13991  ecqusaddd  13994  ghmid  14005  ghminv  14006  imasabl  14092  gsumfzmhm  14099  gsumsplit0  14102  gsumshift  14108  gfsumsn  14110  prdssca  14120  prds0g  14140  mgpress  14173  rnglz  14187  rngrz  14188  rngmneg1  14189  rngmneg2  14190  rngpropd  14197  rng1zrlem  14201  srgmulgass  14235  srgpcomp  14236  srgpcomppsc  14238  ringadd2  14273  ringo2times  14274  ringlz  14289  ringrz  14290  ringinvnzdiv  14296  ringnegl  14297  ringnegr  14298  imasring  14310  qusring2  14312  crngunit  14359  rhmopp  14424  lringuplu  14444  opprdomnbg  14524  lmod0vs  14598  lmodvsmmulgdi  14600  lmodfopne  14603  islss3  14656  lspsn  14693  lmodindp1  14705  rnglidlmmgm  14773  rnglidlmsgrp  14774  rnglidlrng  14775  isridl  14781  zringinvg  14881  zndvds  14926  znf1o  14928  psrgrp  14969  toponcom  15021  tgtopon  15060  restopnb  15175  cnptoprest  15233  blfvalps  15379  bdmopn  15498  cnmet  15524  mpomulcn  15560  limcdifap  15656  dvidsslem  15687  dviaddf  15699  dvexp  15705  dvply2g  15760  coseq0negpitopi  15830  abssinper  15840  rplogbzexp  15948  pellexlem2  15975  dvdsppwf1o  15986  mpodvdsmulf1o  15987  fsumdvdsmul  15988  sgmmul  15993  perfect  15998  lgsvalmod  16021  lgsneg  16026  gausslemma2dlem1a  16060  gausslemma2dlem6  16069  gausslemma2dlem7  16070  gausslemma2d  16071  lgsquadlem2  16080  2lgslem1a1  16088  2lgslem1a  16090  2lgslem3c  16097  2lgslem3d  16098  2lgslem3d1  16102  2lgs  16106  2lgsoddprm  16115  uhgrun  16210  upgrun  16250  umgrun  16252  ushgredgedg  16350  issubgr2  16382  uhgrissubgr  16385  subgruhgredgdm  16394  subumgredg2en  16395  subupgr  16397  p1evtxdeqfilem  16435  wlklenvm1  16465  wlklenvm1g  16466  wlkl1loop  16482  upgriswlkdc  16484  uspgr2wlkeq  16489  uspgr2wlkeq2  16490  uspgr2wlkeqi  16491  wlkres  16503  loopclwwlkn1b  16543  clwwlkn1loopb  16544  clwwlkext2edg  16546  clwwlknonccat  16557  s2elclwwlknon2  16560  clwwlknonex2lem2  16562  clwwlknun  16565  eupth2lem3fi  16600  eupth2lembfi  16601  subctctexmid  16913  cvgcmp2nlemabs  16955  trilpolemlt1  16964