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  2933  dedhb  2988  eqsstrrd  3277  sseqtrrd  3279  eqsstrrdi  3293  dfrab3ss  3501  uneqdifeqim  3597  ifbothdadc  3658  ifbothdc  3659  2if2dc  3664  disjsn2  3754  diftpsn3  3837  elpr2elpr  3882  dfopg  3883  unimax  3950  sndisj  4107  eqbrtrrd  4135  breqtrrd  4139  breqtrrid  4149  eqbrtrrdi  4151  class2seteq  4278  opth1  4354  euotd  4373  opelopabsb  4380  tfisi  4711  0nelxp  4779  opeliunxp  4807  euiotaex  5331  iota4  5334  iotam  5346  fun2ssres  5398  funimass1  5435  funssfv  5698  fnimapr  5739  fvun1  5745  fvco4  5751  elfvmptrab  5775  fmptco  5845  fncofn  5864  foima2  5926  foeqcnvco  5965  f1eqcocnv  5966  f1oiso2  6002  riotass2  6034  riotass  6035  f1ocnvfv3  6041  fvmpopr2d  6192  caovlem2d  6249  f1opw2  6263  offveq  6289  sbcopeq1a  6383  csbopeq1a  6384  eloprabi  6394  cnvf1olem  6422  f2ndf  6424  suppval1  6441  suppsnopdc  6452  smoiso  6535  nnaword  6746  eqer  6801  uniqs  6829  mapsncnv  6932  ixpiinm  6961  mapsnf1o  6974  mapunen  7106  ssenen  7107  findcard2  7148  findcard2s  7149  unsnfidcex  7182  fisseneq  7197  phpeqd  7198  en1eqsn  7220  sbthlemi6  7234  updjud  7375  omp1eomlem  7387  nnnninf2  7420  nninfisollem0  7423  nninfisollemeq  7425  fodju0  7440  3nsssucpw1  7548  enq0sym  7752  enq0tr  7754  recexgt0sr  8093  caucvgsrlemoffcau  8118  axcaucvglemval  8217  le2tri3i  8387  cnegexlem2  8454  nnpcan  8501  addlsub  8648  negf1o  8660  subdi  8663  rereim  8865  cru  8881  divmulassap  8974  divmulasscomap  8975  divap1d  9080  subhalfhalf  9478  div4p1lem1div2  9497  difgtsumgt  9652  elz2  9654  zindd  9702  qapne  9977  divge1  10062  xrlttri3  10136  fseq1p1m1  10435  fzrevral  10446  nn0disj  10479  fzo0addel  10540  fzosplitsnm1  10561  fzosplitprm1  10587  flqlelt  10643  divfl0  10663  flqpmodeq  10696  zmodidfzo  10722  modqmuladd  10735  qnegmod  10738  addmodid  10741  modifeq2int  10755  modqeqmodmin  10763  modfzo0difsn  10764  modsumfzodifsn  10765  addmodlteq  10767  frecuzrdgsuc  10783  frecfzen2  10796  iseqf1olemab  10871  iseqf1olemmo  10874  seqf1oglem1  10888  seqf1oglem2  10889  ser3sub  10892  expgt1  10946  leexp2r  10962  sqoddm1div8  11063  mulsubdivbinom2ap  11081  bcm1k  11130  bcn2m1  11140  hashinfuni  11148  hashennnuni  11150  hashennn  11151  hashunlem  11176  hashprg  11181  fihashssdif  11191  hashfibclem  11214  hashfibc  11215  zfz1isolem1  11220  elovmpowrd  11274  ccatsymb  11298  ccatlid  11302  eqs1  11324  ccatw2s1p1g  11341  swrdfv2  11363  swrds1  11368  swrdlsw  11369  pfxfv  11384  swrdswrd  11405  swrdpfx  11407  pfxpfx  11408  pfxlswccat  11413  ccats1pfxeq  11414  wrdind  11422  wrd2ind  11423  pfxccatin12lem1  11428  pfxccatin12lem2  11431  swrdccat3blem  11439  swrdccat3b  11440  ccats1pfxeqbi  11442  reuccatpfxs1lem  11446  reuccatpfxs1  11447  s3s4d  11503  s2s5d  11504  s5s2d  11505  shftlem  11509  shftfvalg  11511  shftfval  11514  replim  11552  cjexp  11586  resqrexlemcalc1  11707  resqrexlemcvg  11712  rersqrtthlem  11723  abssq  11774  recan  11802  negfi  11921  minclpr  11930  mingeb  11935  xrmaxiflemcom  11942  xrmineqinf  11962  xrminltinf  11965  xrminadd  11968  climmpt  11993  climrecl  12017  fsum3cvg  12072  summodclem3  12074  summodclem2a  12075  modfsummodlemstep  12151  isumsplit  12185  arisum  12192  geosergap  12200  geo2sum  12208  mertenslemi1  12229  mertenslem2  12230  clim2divap  12234  fproddccvg  12266  fprodssdc  12284  fprodabs  12310  fproddivapf  12325  fprodmodd  12335  efcj  12367  efsub  12375  eflegeo  12395  sinneg  12420  cosneg  12421  sin01bnd  12451  cos01bnd  12452  modm1div  12494  summodnegmod  12516  dvdseq  12542  addmodlteqALT  12553  mulmoddvds  12557  zob  12585  nn0ob  12602  divalgmod  12621  flodddiv4  12630  bitsinv1  12656  divgcdnnr  12680  gcdneg  12686  bezoutlemsup  12713  dvdssq  12735  lcmneg  12779  3lcm2e6woprm  12791  6lcm4e12  12792  divgcdcoprmex  12807  cncongr1  12808  cncongrcoprm  12811  oddpwdclemxy  12874  oddpwdclemodd  12877  divnumden  12901  zgcdsq  12906  phibnd  12922  hashgcdlem  12943  vfermltl  12957  powm2modprm  12958  reumodprminv  12959  pythagtriplem19  12988  pcprendvds2  12997  pczpre  13003  dvdsprmpweqle  13043  difsqpwdvds  13044  4sqlem4  13098  ballotfilemfp1  13156  ennnfonelemex  13186  strndxid  13261  topnvalg  13485  prdssca  13509  intopsn  13601  ismgmid2  13614  mgmidsssn0  13618  gsumfzval  13625  gsumprval  13633  mndpfo  13672  mndfo  13673  mndinvmod  13679  prds0g  13683  mnd1id  13690  mhmf1o  13704  0mhm  13720  gsumwmhm  13732  grpidd2  13775  grpinvid2  13787  grpidssd  13810  grpnpcan  13826  grpsubsub4  13827  qusgrp2  13851  mulginvcom  13885  grpissubg  13932  quselbasg  13968  qus0  13973  ecqusaddd  13976  ghmid  13987  ghminv  13988  imasabl  14074  gsumfzmhm  14081  gsumsplit0  14084  mgpress  14096  rnglz  14110  rngrz  14111  rngmneg1  14112  rngmneg2  14113  rngpropd  14120  srg1zr  14152  srgmulgass  14154  srgpcomp  14155  srgpcomppsc  14157  ringadd2  14192  ringo2times  14193  ringlz  14208  ringrz  14209  ringinvnzdiv  14215  ringnegl  14216  ringnegr  14217  imasring  14229  qusring2  14231  crngunit  14278  rhmopp  14343  lringuplu  14363  opprdomnbg  14443  lmod0vs  14518  lmodvsmmulgdi  14520  lmodfopne  14523  islss3  14576  lspsn  14613  lmodindp1  14625  rnglidlmmgm  14693  rnglidlmsgrp  14694  rnglidlrng  14695  isridl  14701  zringinvg  14801  zndvds  14846  znf1o  14848  psrgrp  14889  toponcom  14941  tgtopon  14980  restopnb  15095  cnptoprest  15153  blfvalps  15299  bdmopn  15418  cnmet  15444  mpomulcn  15480  limcdifap  15576  dvidsslem  15607  dviaddf  15619  dvexp  15625  dvply2g  15680  coseq0negpitopi  15750  abssinper  15760  rplogbzexp  15868  pellexlem2  15895  dvdsppwf1o  15906  mpodvdsmulf1o  15907  fsumdvdsmul  15908  sgmmul  15913  perfect  15918  lgsvalmod  15941  lgsneg  15946  gausslemma2dlem1a  15980  gausslemma2dlem6  15989  gausslemma2dlem7  15990  gausslemma2d  15991  lgsquadlem2  16000  2lgslem1a1  16008  2lgslem1a  16010  2lgslem3c  16017  2lgslem3d  16018  2lgslem3d1  16022  2lgs  16026  2lgsoddprm  16035  uhgrun  16130  upgrun  16170  umgrun  16172  ushgredgedg  16270  issubgr2  16302  uhgrissubgr  16305  subgruhgredgdm  16314  subumgredg2en  16315  subupgr  16317  p1evtxdeqfilem  16355  wlklenvm1  16385  wlklenvm1g  16386  wlkl1loop  16402  upgriswlkdc  16404  uspgr2wlkeq  16409  uspgr2wlkeq2  16410  uspgr2wlkeqi  16411  wlkres  16423  loopclwwlkn1b  16463  clwwlkn1loopb  16464  clwwlkext2edg  16466  clwwlknonccat  16477  s2elclwwlknon2  16480  clwwlknonex2lem2  16482  clwwlknun  16485  eupth2lem3fi  16520  eupth2lembfi  16521  subctctexmid  16823  cvgcmp2nlemabs  16865  trilpolemlt1  16874  gsumgfsumlem  16914  gfsumsn  16916