Theorem eqcomd 2235

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-ext 2211

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

This theorem is referenced by:  eqtr2d  2263  eqtr3d  2264  eqtr4d  2265  eqtr2id  2275  eqtr2di  2279  sylan9req  2283  eqeltrrd  2307  eleqtrrd  2309  eleqtrrid  2319  eqeltrrdi  2321  eqnetrrd  2426  neeqtrrd  2430  rspcedeq2vd  2917  dedhb  2972  eqsstrrd  3261  sseqtrrd  3263  eqsstrrdi  3277  dfrab3ss  3482  uneqdifeqim  3577  ifbothdadc  3636  ifbothdc  3637  2if2dc  3642  disjsn2  3729  diftpsn3  3809  elpr2elpr  3854  dfopg  3855  unimax  3922  sndisj  4079  eqbrtrrd  4107  breqtrrd  4111  breqtrrid  4121  eqbrtrrdi  4123  class2seteq  4247  opth1  4322  euotd  4341  opelopabsb  4348  tfisi  4679  0nelxp  4747  opeliunxp  4774  euiotaex  5295  iota4  5298  iotam  5310  fun2ssres  5361  funimass1  5398  funssfv  5655  fnimapr  5696  fvun1  5702  fvco4  5708  elfvmptrab  5732  fmptco  5803  fncofn  5821  foima2  5881  foeqcnvco  5920  f1eqcocnv  5921  f1oiso2  5957  riotass2  5989  riotass  5990  f1ocnvfv3  5996  fvmpopr2d  6147  caovlem2d  6204  f1opw2  6218  offveq  6245  sbcopeq1a  6339  csbopeq1a  6340  eloprabi  6348  cnvf1olem  6376  f2ndf  6378  smoiso  6454  nnaword  6665  eqer  6720  uniqs  6748  mapsncnv  6850  ixpiinm  6879  mapsnf1o  6892  ssenen  7020  findcard2  7059  findcard2s  7060  unsnfidcex  7090  fisseneq  7104  phpeqd  7105  en1eqsn  7123  sbthlemi6  7137  updjud  7257  omp1eomlem  7269  nnnninf2  7302  nninfisollem0  7305  nninfisollemeq  7307  fodju0  7322  3nsssucpw1  7429  enq0sym  7627  enq0tr  7629  recexgt0sr  7968  caucvgsrlemoffcau  7993  axcaucvglemval  8092  le2tri3i  8263  cnegexlem2  8330  nnpcan  8377  addlsub  8524  negf1o  8536  subdi  8539  rereim  8741  cru  8757  divmulassap  8850  divmulasscomap  8851  divap1d  8956  subhalfhalf  9354  div4p1lem1div2  9373  difgtsumgt  9524  elz2  9526  zindd  9573  qapne  9842  divge1  9927  xrlttri3  10001  fseq1p1m1  10298  fzrevral  10309  nn0disj  10342  fzo0addel  10402  fzosplitsnm1  10423  fzosplitprm1  10448  flqlelt  10504  divfl0  10524  flqpmodeq  10557  zmodidfzo  10583  modqmuladd  10596  qnegmod  10599  addmodid  10602  modifeq2int  10616  modqeqmodmin  10624  modfzo0difsn  10625  modsumfzodifsn  10626  addmodlteq  10628  frecuzrdgsuc  10644  frecfzen2  10657  iseqf1olemab  10732  iseqf1olemmo  10735  seqf1oglem1  10749  seqf1oglem2  10750  ser3sub  10753  expgt1  10807  leexp2r  10823  sqoddm1div8  10923  mulsubdivbinom2ap  10941  bcm1k  10990  bcn2m1  10999  hashinfuni  11007  hashennnuni  11009  hashennn  11010  hashunlem  11034  hashprg  11038  fihashssdif  11048  zfz1isolem1  11070  elovmpowrd  11121  ccatsymb  11145  ccatlid  11149  eqs1  11169  swrdfv2  11203  swrds1  11208  swrdlsw  11209  pfxfv  11224  swrdswrd  11245  swrdpfx  11247  pfxpfx  11248  pfxlswccat  11253  ccats1pfxeq  11254  wrdind  11262  wrd2ind  11263  pfxccatin12lem1  11268  pfxccatin12lem2  11271  swrdccat3blem  11279  swrdccat3b  11280  ccats1pfxeqbi  11282  reuccatpfxs1lem  11286  reuccatpfxs1  11287  shftlem  11335  shftfvalg  11337  shftfval  11340  replim  11378  cjexp  11412  resqrexlemcalc1  11533  resqrexlemcvg  11538  rersqrtthlem  11549  abssq  11600  recan  11628  negfi  11747  minclpr  11756  mingeb  11761  xrmaxiflemcom  11768  xrmineqinf  11788  xrminltinf  11791  xrminadd  11794  climmpt  11819  climrecl  11843  fsum3cvg  11897  summodclem3  11899  summodclem2a  11900  modfsummodlemstep  11976  isumsplit  12010  arisum  12017  geosergap  12025  geo2sum  12033  mertenslemi1  12054  mertenslem2  12055  clim2divap  12059  fproddccvg  12091  fprodssdc  12109  fprodabs  12135  fproddivapf  12150  fprodmodd  12160  efcj  12192  efsub  12200  eflegeo  12220  sinneg  12245  cosneg  12246  sin01bnd  12276  cos01bnd  12277  modm1div  12319  summodnegmod  12341  dvdseq  12367  addmodlteqALT  12378  mulmoddvds  12382  zob  12410  nn0ob  12427  divalgmod  12446  flodddiv4  12455  bitsinv1  12481  divgcdnnr  12505  gcdneg  12511  bezoutlemsup  12538  dvdssq  12560  lcmneg  12604  3lcm2e6woprm  12616  6lcm4e12  12617  divgcdcoprmex  12632  cncongr1  12633  cncongrcoprm  12636  oddpwdclemxy  12699  oddpwdclemodd  12702  divnumden  12726  zgcdsq  12731  phibnd  12747  hashgcdlem  12768  vfermltl  12782  powm2modprm  12783  reumodprminv  12784  pythagtriplem19  12813  pcprendvds2  12822  pczpre  12828  dvdsprmpweqle  12868  difsqpwdvds  12869  4sqlem4  12923  ennnfonelemex  12993  strndxid  13068  topnvalg  13292  prdssca  13316  intopsn  13408  ismgmid2  13421  mgmidsssn0  13425  gsumfzval  13432  gsumprval  13440  mndpfo  13479  mndfo  13480  mndinvmod  13486  prds0g  13490  mnd1id  13497  mhmf1o  13511  0mhm  13527  gsumwmhm  13539  grpidd2  13582  grpinvid2  13594  grpidssd  13617  grpnpcan  13633  grpsubsub4  13634  qusgrp2  13658  mulginvcom  13692  grpissubg  13739  quselbasg  13775  qus0  13780  ecqusaddd  13783  ghmid  13794  ghminv  13795  imasabl  13881  gsumfzmhm  13888  mgpress  13902  rnglz  13916  rngrz  13917  rngmneg1  13918  rngmneg2  13919  rngpropd  13926  srg1zr  13958  srgmulgass  13960  srgpcomp  13961  srgpcomppsc  13963  ringadd2  13998  ringo2times  13999  ringlz  14014  ringrz  14015  ringinvnzdiv  14021  ringnegl  14022  ringnegr  14023  imasring  14035  qusring2  14037  crngunit  14083  rhmopp  14148  lringuplu  14168  opprdomnbg  14246  lmod0vs  14293  lmodvsmmulgdi  14295  lmodfopne  14298  islss3  14351  lspsn  14388  lmodindp1  14400  rnglidlmmgm  14468  rnglidlmsgrp  14469  rnglidlrng  14470  isridl  14476  zringinvg  14576  zndvds  14621  znf1o  14623  psrgrp  14657  toponcom  14709  tgtopon  14748  restopnb  14863  cnptoprest  14921  blfvalps  15067  bdmopn  15186  cnmet  15212  mpomulcn  15248  limcdifap  15344  dvidsslem  15375  dviaddf  15387  dvexp  15393  dvply2g  15448  coseq0negpitopi  15518  abssinper  15528  rplogbzexp  15636  dvdsppwf1o  15671  mpodvdsmulf1o  15672  fsumdvdsmul  15673  sgmmul  15678  perfect  15683  lgsvalmod  15706  lgsneg  15711  gausslemma2dlem1a  15745  gausslemma2dlem6  15754  gausslemma2dlem7  15755  gausslemma2d  15756  lgsquadlem2  15765  2lgslem1a1  15773  2lgslem1a  15775  2lgslem3c  15782  2lgslem3d  15783  2lgslem3d1  15787  2lgs  15791  2lgsoddprm  15800  uhgrun  15894  upgrun  15932  umgrun  15934  ushgredgedg  16032  wlklenvm1  16062  wlklenvm1g  16063  wlkl1loop  16079  upgriswlkdc  16081  uspgr2wlkeq  16086  uspgr2wlkeq2  16087  uspgr2wlkeqi  16088  wlkres  16098  subctctexmid  16395  cvgcmp2nlemabs  16430  trilpolemlt1  16439