Theorem eqcomd 2235

Description: Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)

Hypothesis

Ref	Expression
eqcomd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
eqcomd	|- ( ph -> B = A )

Proof of Theorem eqcomd

Step	Hyp	Ref	Expression
1		eqcomd.1	. 2 |- ( ph -> A = B )
2		eqcom 2231	. 2 |- ( A = B <-> B = A )
3	1, 2	sylib 122	1 |- ( ph -> B = A )

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  7071  findcard2s  7072  unsnfidcex  7105  fisseneq  7119  phpeqd  7120  en1eqsn  7138  sbthlemi6  7152  updjud  7272  omp1eomlem  7284  nnnninf2  7317  nninfisollem0  7320  nninfisollemeq  7322  fodju0  7337  3nsssucpw1  7444  enq0sym  7642  enq0tr  7644  recexgt0sr  7983  caucvgsrlemoffcau  8008  axcaucvglemval  8107  le2tri3i  8278  cnegexlem2  8345  nnpcan  8392  addlsub  8539  negf1o  8551  subdi  8554  rereim  8756  cru  8772  divmulassap  8865  divmulasscomap  8866  divap1d  8971  subhalfhalf  9369  div4p1lem1div2  9388  difgtsumgt  9539  elz2  9541  zindd  9588  qapne  9863  divge1  9948  xrlttri3  10022  fseq1p1m1  10319  fzrevral  10330  nn0disj  10363  fzo0addel  10423  fzosplitsnm1  10444  fzosplitprm1  10470  flqlelt  10526  divfl0  10546  flqpmodeq  10579  zmodidfzo  10605  modqmuladd  10618  qnegmod  10621  addmodid  10624  modifeq2int  10638  modqeqmodmin  10646  modfzo0difsn  10647  modsumfzodifsn  10648  addmodlteq  10650  frecuzrdgsuc  10666  frecfzen2  10679  iseqf1olemab  10754  iseqf1olemmo  10757  seqf1oglem1  10771  seqf1oglem2  10772  ser3sub  10775  expgt1  10829  leexp2r  10845  sqoddm1div8  10945  mulsubdivbinom2ap  10963  bcm1k  11012  bcn2m1  11021  hashinfuni  11029  hashennnuni  11031  hashennn  11032  hashunlem  11057  hashprg  11062  fihashssdif  11072  zfz1isolem1  11094  elovmpowrd  11145  ccatsymb  11169  ccatlid  11173  eqs1  11195  ccatw2s1p1g  11212  swrdfv2  11234  swrds1  11239  swrdlsw  11240  pfxfv  11255  swrdswrd  11276  swrdpfx  11278  pfxpfx  11279  pfxlswccat  11284  ccats1pfxeq  11285  wrdind  11293  wrd2ind  11294  pfxccatin12lem1  11299  pfxccatin12lem2  11302  swrdccat3blem  11310  swrdccat3b  11311  ccats1pfxeqbi  11313  reuccatpfxs1lem  11317  reuccatpfxs1  11318  shftlem  11367  shftfvalg  11369  shftfval  11372  replim  11410  cjexp  11444  resqrexlemcalc1  11565  resqrexlemcvg  11570  rersqrtthlem  11581  abssq  11632  recan  11660  negfi  11779  minclpr  11788  mingeb  11793  xrmaxiflemcom  11800  xrmineqinf  11820  xrminltinf  11823  xrminadd  11826  climmpt  11851  climrecl  11875  fsum3cvg  11929  summodclem3  11931  summodclem2a  11932  modfsummodlemstep  12008  isumsplit  12042  arisum  12049  geosergap  12057  geo2sum  12065  mertenslemi1  12086  mertenslem2  12087  clim2divap  12091  fproddccvg  12123  fprodssdc  12141  fprodabs  12167  fproddivapf  12182  fprodmodd  12192  efcj  12224  efsub  12232  eflegeo  12252  sinneg  12277  cosneg  12278  sin01bnd  12308  cos01bnd  12309  modm1div  12351  summodnegmod  12373  dvdseq  12399  addmodlteqALT  12410  mulmoddvds  12414  zob  12442  nn0ob  12459  divalgmod  12478  flodddiv4  12487  bitsinv1  12513  divgcdnnr  12537  gcdneg  12543  bezoutlemsup  12570  dvdssq  12592  lcmneg  12636  3lcm2e6woprm  12648  6lcm4e12  12649  divgcdcoprmex  12664  cncongr1  12665  cncongrcoprm  12668  oddpwdclemxy  12731  oddpwdclemodd  12734  divnumden  12758  zgcdsq  12763  phibnd  12779  hashgcdlem  12800  vfermltl  12814  powm2modprm  12815  reumodprminv  12816  pythagtriplem19  12845  pcprendvds2  12854  pczpre  12860  dvdsprmpweqle  12900  difsqpwdvds  12901  4sqlem4  12955  ennnfonelemex  13025  strndxid  13100  topnvalg  13324  prdssca  13348  intopsn  13440  ismgmid2  13453  mgmidsssn0  13457  gsumfzval  13464  gsumprval  13472  mndpfo  13511  mndfo  13512  mndinvmod  13518  prds0g  13522  mnd1id  13529  mhmf1o  13543  0mhm  13559  gsumwmhm  13571  grpidd2  13614  grpinvid2  13626  grpidssd  13649  grpnpcan  13665  grpsubsub4  13666  qusgrp2  13690  mulginvcom  13724  grpissubg  13771  quselbasg  13807  qus0  13812  ecqusaddd  13815  ghmid  13826  ghminv  13827  imasabl  13913  gsumfzmhm  13920  mgpress  13934  rnglz  13948  rngrz  13949  rngmneg1  13950  rngmneg2  13951  rngpropd  13958  srg1zr  13990  srgmulgass  13992  srgpcomp  13993  srgpcomppsc  13995  ringadd2  14030  ringo2times  14031  ringlz  14046  ringrz  14047  ringinvnzdiv  14053  ringnegl  14054  ringnegr  14055  imasring  14067  qusring2  14069  crngunit  14115  rhmopp  14180  lringuplu  14200  opprdomnbg  14278  lmod0vs  14325  lmodvsmmulgdi  14327  lmodfopne  14330  islss3  14383  lspsn  14420  lmodindp1  14432  rnglidlmmgm  14500  rnglidlmsgrp  14501  rnglidlrng  14502  isridl  14508  zringinvg  14608  zndvds  14653  znf1o  14655  psrgrp  14689  toponcom  14741  tgtopon  14780  restopnb  14895  cnptoprest  14953  blfvalps  15099  bdmopn  15218  cnmet  15244  mpomulcn  15280  limcdifap  15376  dvidsslem  15407  dviaddf  15419  dvexp  15425  dvply2g  15480  coseq0negpitopi  15550  abssinper  15560  rplogbzexp  15668  dvdsppwf1o  15703  mpodvdsmulf1o  15704  fsumdvdsmul  15705  sgmmul  15710  perfect  15715  lgsvalmod  15738  lgsneg  15743  gausslemma2dlem1a  15777  gausslemma2dlem6  15786  gausslemma2dlem7  15787  gausslemma2d  15788  lgsquadlem2  15797  2lgslem1a1  15805  2lgslem1a  15807  2lgslem3c  15814  2lgslem3d  15815  2lgslem3d1  15819  2lgs  15823  2lgsoddprm  15832  uhgrun  15927  upgrun  15965  umgrun  15967  ushgredgedg  16065  wlklenvm1  16138  wlklenvm1g  16139  wlkl1loop  16155  upgriswlkdc  16157  uspgr2wlkeq  16162  uspgr2wlkeq2  16163  uspgr2wlkeqi  16164  wlkres  16174  loopclwwlkn1b  16214  clwwlkn1loopb  16215  clwwlkext2edg  16217  clwwlknonccat  16228  s2elclwwlknon2  16231  clwwlknonex2lem2  16233  clwwlknun  16236  subctctexmid  16537  cvgcmp2nlemabs  16572  trilpolemlt1  16581