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  2918  dedhb  2973  eqsstrrd  3262  sseqtrrd  3264  eqsstrrdi  3278  dfrab3ss  3483  uneqdifeqim  3578  ifbothdadc  3637  ifbothdc  3638  2if2dc  3643  disjsn2  3730  diftpsn3  3812  elpr2elpr  3857  dfopg  3858  unimax  3925  sndisj  4082  eqbrtrrd  4110  breqtrrd  4114  breqtrrid  4124  eqbrtrrdi  4126  class2seteq  4251  opth1  4326  euotd  4345  opelopabsb  4352  tfisi  4683  0nelxp  4751  opeliunxp  4779  euiotaex  5301  iota4  5304  iotam  5316  fun2ssres  5367  funimass1  5404  funssfv  5661  fnimapr  5702  fvun1  5708  fvco4  5714  elfvmptrab  5738  fmptco  5809  fncofn  5827  foima2  5887  foeqcnvco  5926  f1eqcocnv  5927  f1oiso2  5963  riotass2  5995  riotass  5996  f1ocnvfv3  6002  fvmpopr2d  6153  caovlem2d  6210  f1opw2  6224  offveq  6251  sbcopeq1a  6345  csbopeq1a  6346  eloprabi  6356  cnvf1olem  6384  f2ndf  6386  smoiso  6463  nnaword  6674  eqer  6729  uniqs  6757  mapsncnv  6859  ixpiinm  6888  mapsnf1o  6901  ssenen  7032  findcard2  7073  findcard2s  7074  unsnfidcex  7107  fisseneq  7121  phpeqd  7122  en1eqsn  7141  sbthlemi6  7155  updjud  7275  omp1eomlem  7287  nnnninf2  7320  nninfisollem0  7323  nninfisollemeq  7325  fodju0  7340  3nsssucpw1  7447  enq0sym  7645  enq0tr  7647  recexgt0sr  7986  caucvgsrlemoffcau  8011  axcaucvglemval  8110  le2tri3i  8281  cnegexlem2  8348  nnpcan  8395  addlsub  8542  negf1o  8554  subdi  8557  rereim  8759  cru  8775  divmulassap  8868  divmulasscomap  8869  divap1d  8974  subhalfhalf  9372  div4p1lem1div2  9391  difgtsumgt  9542  elz2  9544  zindd  9591  qapne  9866  divge1  9951  xrlttri3  10025  fseq1p1m1  10322  fzrevral  10333  nn0disj  10366  fzo0addel  10426  fzosplitsnm1  10447  fzosplitprm1  10473  flqlelt  10529  divfl0  10549  flqpmodeq  10582  zmodidfzo  10608  modqmuladd  10621  qnegmod  10624  addmodid  10627  modifeq2int  10641  modqeqmodmin  10649  modfzo0difsn  10650  modsumfzodifsn  10651  addmodlteq  10653  frecuzrdgsuc  10669  frecfzen2  10682  iseqf1olemab  10757  iseqf1olemmo  10760  seqf1oglem1  10774  seqf1oglem2  10775  ser3sub  10778  expgt1  10832  leexp2r  10848  sqoddm1div8  10948  mulsubdivbinom2ap  10966  bcm1k  11015  bcn2m1  11024  hashinfuni  11032  hashennnuni  11034  hashennn  11035  hashunlem  11060  hashprg  11065  fihashssdif  11075  zfz1isolem1  11097  elovmpowrd  11148  ccatsymb  11172  ccatlid  11176  eqs1  11198  ccatw2s1p1g  11215  swrdfv2  11237  swrds1  11242  swrdlsw  11243  pfxfv  11258  swrdswrd  11279  swrdpfx  11281  pfxpfx  11282  pfxlswccat  11287  ccats1pfxeq  11288  wrdind  11296  wrd2ind  11297  pfxccatin12lem1  11302  pfxccatin12lem2  11305  swrdccat3blem  11313  swrdccat3b  11314  ccats1pfxeqbi  11316  reuccatpfxs1lem  11320  reuccatpfxs1  11321  shftlem  11370  shftfvalg  11372  shftfval  11375  replim  11413  cjexp  11447  resqrexlemcalc1  11568  resqrexlemcvg  11573  rersqrtthlem  11584  abssq  11635  recan  11663  negfi  11782  minclpr  11791  mingeb  11796  xrmaxiflemcom  11803  xrmineqinf  11823  xrminltinf  11826  xrminadd  11829  climmpt  11854  climrecl  11878  fsum3cvg  11932  summodclem3  11934  summodclem2a  11935  modfsummodlemstep  12011  isumsplit  12045  arisum  12052  geosergap  12060  geo2sum  12068  mertenslemi1  12089  mertenslem2  12090  clim2divap  12094  fproddccvg  12126  fprodssdc  12144  fprodabs  12170  fproddivapf  12185  fprodmodd  12195  efcj  12227  efsub  12235  eflegeo  12255  sinneg  12280  cosneg  12281  sin01bnd  12311  cos01bnd  12312  modm1div  12354  summodnegmod  12376  dvdseq  12402  addmodlteqALT  12413  mulmoddvds  12417  zob  12445  nn0ob  12462  divalgmod  12481  flodddiv4  12490  bitsinv1  12516  divgcdnnr  12540  gcdneg  12546  bezoutlemsup  12573  dvdssq  12595  lcmneg  12639  3lcm2e6woprm  12651  6lcm4e12  12652  divgcdcoprmex  12667  cncongr1  12668  cncongrcoprm  12671  oddpwdclemxy  12734  oddpwdclemodd  12737  divnumden  12761  zgcdsq  12766  phibnd  12782  hashgcdlem  12803  vfermltl  12817  powm2modprm  12818  reumodprminv  12819  pythagtriplem19  12848  pcprendvds2  12857  pczpre  12863  dvdsprmpweqle  12903  difsqpwdvds  12904  4sqlem4  12958  ennnfonelemex  13028  strndxid  13103  topnvalg  13327  prdssca  13351  intopsn  13443  ismgmid2  13456  mgmidsssn0  13460  gsumfzval  13467  gsumprval  13475  mndpfo  13514  mndfo  13515  mndinvmod  13521  prds0g  13525  mnd1id  13532  mhmf1o  13546  0mhm  13562  gsumwmhm  13574  grpidd2  13617  grpinvid2  13629  grpidssd  13652  grpnpcan  13668  grpsubsub4  13669  qusgrp2  13693  mulginvcom  13727  grpissubg  13774  quselbasg  13810  qus0  13815  ecqusaddd  13818  ghmid  13829  ghminv  13830  imasabl  13916  gsumfzmhm  13923  mgpress  13937  rnglz  13951  rngrz  13952  rngmneg1  13953  rngmneg2  13954  rngpropd  13961  srg1zr  13993  srgmulgass  13995  srgpcomp  13996  srgpcomppsc  13998  ringadd2  14033  ringo2times  14034  ringlz  14049  ringrz  14050  ringinvnzdiv  14056  ringnegl  14057  ringnegr  14058  imasring  14070  qusring2  14072  crngunit  14118  rhmopp  14183  lringuplu  14203  opprdomnbg  14281  lmod0vs  14328  lmodvsmmulgdi  14330  lmodfopne  14333  islss3  14386  lspsn  14423  lmodindp1  14435  rnglidlmmgm  14503  rnglidlmsgrp  14504  rnglidlrng  14505  isridl  14511  zringinvg  14611  zndvds  14656  znf1o  14658  psrgrp  14692  toponcom  14744  tgtopon  14783  restopnb  14898  cnptoprest  14956  blfvalps  15102  bdmopn  15221  cnmet  15247  mpomulcn  15283  limcdifap  15379  dvidsslem  15410  dviaddf  15422  dvexp  15428  dvply2g  15483  coseq0negpitopi  15553  abssinper  15563  rplogbzexp  15671  dvdsppwf1o  15706  mpodvdsmulf1o  15707  fsumdvdsmul  15708  sgmmul  15713  perfect  15718  lgsvalmod  15741  lgsneg  15746  gausslemma2dlem1a  15780  gausslemma2dlem6  15789  gausslemma2dlem7  15790  gausslemma2d  15791  lgsquadlem2  15800  2lgslem1a1  15808  2lgslem1a  15810  2lgslem3c  15817  2lgslem3d  15818  2lgslem3d1  15822  2lgs  15826  2lgsoddprm  15835  uhgrun  15930  upgrun  15970  umgrun  15972  ushgredgedg  16070  p1evtxdeqfilem  16122  wlklenvm1  16152  wlklenvm1g  16153  wlkl1loop  16169  upgriswlkdc  16171  uspgr2wlkeq  16176  uspgr2wlkeq2  16177  uspgr2wlkeqi  16178  wlkres  16188  loopclwwlkn1b  16228  clwwlkn1loopb  16229  clwwlkext2edg  16231  clwwlknonccat  16242  s2elclwwlknon2  16245  clwwlknonex2lem2  16247  clwwlknun  16250  subctctexmid  16551  cvgcmp2nlemabs  16586  trilpolemlt1  16595  gsumgfsumlem  16633