Theorem eqcomd 2244

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

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-ext 2220

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

This theorem is referenced by:  eqtr2d  2272  eqtr3d  2273  eqtr4d  2274  eqtr2id  2284  eqtr2di  2288  sylan9req  2292  eqeltrrd  2316  eleqtrrd  2318  eleqtrrid  2328  eqeltrrdi  2330  eqabcdv  2370  eqnetrrd  2446  neeqtrrd  2450  rspcedeq2vd  2940  dedhb  2995  eqsstrrd  3285  sseqtrrd  3287  eqsstrrdi  3301  dfrab3ss  3511  uneqdifeqim  3613  ifbothdadc  3674  ifbothdc  3675  2if2dc  3680  ifeqeqxdc  3687  disjsn2  3771  diftpsn3  3854  elpr2elpr  3899  dfopg  3900  unimax  3967  sndisj  4124  eqbrtrrd  4152  breqtrrd  4156  breqtrrid  4166  eqbrtrrdi  4168  class2seteq  4298  opth1  4374  euotd  4393  opelopabsb  4400  tfisi  4732  0nelxp  4800  opeliunxp  4828  euiotaex  5352  iota4  5355  iotam  5367  fun2ssres  5419  funimass1  5456  funssfv  5719  fnimapr  5760  fvun1  5766  fvco4  5774  elfvmptrab  5798  fmptco  5868  fncofn  5887  foima2  5951  foeqcnvco  5990  f1eqcocnv  5991  f1oiso2  6027  riotass2  6061  riotass  6062  f1ocnvfv3  6068  fvmpopr2d  6219  caovlem2d  6276  f1opw2  6290  offveq  6317  sbcopeq1a  6415  csbopeq1a  6416  eloprabi  6426  cnvf1olem  6454  f2ndf  6456  suppval1  6473  suppsnopdc  6484  smoiso  6567  nnaword  6778  eqer  6833  uniqs  6861  mapsncnv  6971  ixpiinm  7000  mapsnf1o  7013  mapunen  7145  ssenen  7146  findcard2  7187  findcard2s  7188  unsnfidcex  7221  fisseneq  7236  phpeqd  7237  en1eqsn  7259  sbthlemi6  7273  updjud  7416  omp1eomlem  7428  nnnninf2  7461  nninfisollem0  7464  nninfisollemeq  7466  fodju0  7481  3nsssucpw1  7589  enq0sym  7793  enq0tr  7795  recexgt0sr  8134  caucvgsrlemoffcau  8159  axcaucvglemval  8258  le2tri3i  8428  cnegexlem2  8496  nnpcan  8543  addlsub  8690  negf1o  8703  subdi  8706  rereim  8908  cru  8924  divmulassap  9019  divmulasscomap  9020  divap1d  9125  subhalfhalf  9523  div4p1lem1div2  9542  difgtsumgt  9697  elz2  9699  zindd  9747  qapne  10022  divge1  10107  xrlttri3  10182  fseq1p1m1  10484  fzrevral  10495  nn0disj  10528  fzo0addel  10589  fzosplitsnm1  10610  fzosplitprm1  10636  flqlelt  10694  divfl0  10714  flqpmodeq  10747  zmodidfzo  10773  modqmuladd  10786  qnegmod  10789  addmodid  10792  modifeq2int  10806  modqeqmodmin  10814  modfzo0difsn  10815  modsumfzodifsn  10816  addmodlteq  10818  frecuzrdgsuc  10834  frecfzen2  10847  iseqf1olemab  10922  iseqf1olemmo  10925  seqf1oglem1  10939  seqf1oglem2  10940  ser3sub  10943  expgt1  10997  leexp2r  11013  sqoddm1div8  11114  mulsubdivbinom2ap  11132  bcm1k  11181  bcn2m1  11191  hashinfuni  11199  hashennnuni  11201  hashennn  11202  hashunlem  11227  hashprg  11232  fihashssdif  11242  hashfibclem  11265  hashfibc  11266  hashf1lem1  11268  hashf1lem2  11269  zfz1isolem1  11275  elovmpowrd  11329  ccatsymb  11353  ccatlid  11357  eqs1  11379  ccatw2s1p1g  11396  swrdfv2  11418  swrds1  11423  swrdlsw  11424  pfxfv  11439  swrdswrd  11460  swrdpfx  11462  pfxpfx  11463  pfxlswccat  11468  ccats1pfxeq  11469  wrdind  11477  wrd2ind  11478  pfxccatin12lem1  11483  pfxccatin12lem2  11486  swrdccat3blem  11494  swrdccat3b  11495  ccats1pfxeqbi  11497  reuccatpfxs1lem  11501  reuccatpfxs1  11502  s3s4d  11558  s2s5d  11559  s5s2d  11560  shftlem  11564  shftfvalg  11566  shftfval  11569  replim  11607  cjexp  11641  sq01  11643  resqrexlemcalc1  11763  resqrexlemcvg  11768  rersqrtthlem  11779  abssq  11830  recan  11858  negfi  11977  minclpr  11986  mingeb  11991  xrmaxiflemcom  11998  xrmineqinf  12018  xrminltinf  12021  xrminadd  12024  climmpt  12049  climrecl  12073  fsum3cvg  12128  summodclem3  12130  summodclem2a  12131  modfsummodlemstep  12207  isumsplit  12241  arisum  12248  geosergap  12256  geo2sum  12264  mertenslemi1  12285  mertenslem2  12286  clim2divap  12290  fproddccvg  12322  fprodssdc  12340  fprodabs  12366  fproddivapf  12381  fprodmodd  12391  efcj  12423  efsub  12431  eflegeo  12451  sinneg  12476  cosneg  12477  sin01bnd  12507  cos01bnd  12508  modm1div  12550  summodnegmod  12572  dvdseq  12598  addmodlteqALT  12609  mulmoddvds  12613  zob  12641  nn0ob  12658  divalgmod  12677  flodddiv4  12686  bitsinv1  12712  divgcdnnr  12736  gcdneg  12742  bezoutlemsup  12769  dvdssq  12791  lcmneg  12835  3lcm2e6woprm  12847  6lcm4e12  12848  divgcdcoprmex  12863  cncongr1  12864  cncongrcoprm  12867  oddpwdclemxy  12930  oddpwdclemodd  12933  divnumden  12957  zgcdsq  12962  phibnd  12978  hashgcdlem  12999  vfermltl  13013  powm2modprm  13014  reumodprminv  13015  pythagtriplem19  13044  pcprendvds2  13053  pczpre  13059  dvdsprmpweqle  13099  difsqpwdvds  13100  4sqlem4  13154  ballotfilemfp1  13214  ballotfilemsf1o  13240  ballotfilemrinv0  13259  ennnfonelemex  13288  strndxid  13363  topnvalg  13588  intopsn  13670  ismgmid2  13683  mgmidsssn0  13687  gzsumfzval  13694  mndpfo  13734  mndfo  13735  mndinvmod  13741  mnd1id  13746  mhmf1o  13760  0mhm  13776  gzsumwmhm  13786  grpidd2  13829  grpinvid2  13841  grpidssd  13864  grpnpcan  13880  grpsubsub4  13881  qusgrp2  13899  mulginvcom  13933  grpissubg  13980  quselbasg  14016  qus0  14021  ecqusaddd  14024  ghmid  14035  ghminv  14036  imasabl  14123  gzsummhm  14128  gzsumsplit0  14131  gzsumshift  14132  gsumsncmn  14139  prdssca  14158  prds0g  14178  mgpress  14213  rnglz  14227  rngrz  14228  rngmneg1  14229  rngmneg2  14230  rngpropd  14237  rng1zrlem  14241  srgmulgass  14276  srgpcomp  14277  srgpcomppsc  14279  ringadd2  14315  ringo2times  14316  ringlz  14331  ringrz  14332  ringinvnzdiv  14338  ringnegl  14339  ringnegr  14340  imasring  14352  qusring2  14354  crngunit  14401  rhmopp  14466  lringuplu  14486  opprdomnbg  14566  lmod0vs  14641  lmodvsmmulgdi  14643  lmodfopne  14646  islss3  14699  lspsn  14736  lmodindp1  14748  rnglidlmmgm  14816  rnglidlmsgrp  14817  rnglidlrng  14818  isridl  14824  zringinvg  14922  zndvds  14967  znf1o  14969  assa2ass  14992  assa2ass2  14993  asclinvg  15015  assamulgscmlem1  15024  assamulgscmlem2  15025  psrgrp  15059  toponcom  15111  tgtopon  15150  restopnb  15265  cnptoprest  15323  blfvalps  15469  bdmopn  15588  cnmet  15614  mpomulcn  15650  limcdifap  15746  dvidsslem  15777  dviaddf  15789  dvexp  15795  dvply2g  15850  coseq0negpitopi  15920  abssinper  15930  rplogbzexp  16039  pellexlem2  16075  dvdsppwf1o  16086  mpodvdsmulf1o  16087  fsumdvdsmul  16088  sgmmul  16093  perfect  16098  lgsvalmod  16121  lgsneg  16126  gausslemma2dlem1a  16160  gausslemma2dlem6  16169  gausslemma2dlem7  16170  gausslemma2d  16171  lgsquadlem2  16180  2lgslem1a1  16188  2lgslem1a  16190  2lgslem3c  16197  2lgslem3d  16198  2lgslem3d1  16202  2lgs  16206  2lgsoddprm  16215  uhgrun  16310  upgrun  16350  umgrun  16352  ushgredgedg  16450  issubgr2  16482  uhgrissubgr  16485  subgruhgredgdm  16494  subumgredg2en  16495  subupgr  16497  p1evtxdeqfilem  16535  wlklenvm1  16565  wlklenvm1g  16566  wlkl1loop  16582  upgriswlkdc  16584  uspgr2wlkeq  16589  uspgr2wlkeq2  16590  uspgr2wlkeqi  16591  wlkres  16603  loopclwwlkn1b  16643  clwwlkn1loopb  16644  clwwlkext2edg  16646  clwwlknonccat  16657  s2elclwwlknon2  16660  clwwlknonex2lem2  16662  clwwlknun  16665  eupth2lem3fi  16700  eupth2lembfi  16701  subctctexmid  17013  cvgcmp2nlemabs  17055  trilpolemlt1  17064