Theorem eqcomd 2100

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 2097	. 2 |- ( A = B <-> B = A )
3	1, 2	sylib 121	1 |- ( ph -> B = A )

Syntax hints:   -> wi 4   = wceq 1296

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-cleq 2088

This theorem is referenced by:  eqtr2d  2128  eqtr3d  2129  eqtr4d  2130  syl5req  2140  syl6req  2144  sylan9req  2148  eqeltrrd  2172  eleqtrrd  2174  syl5eleqr  2184  syl6eqelr  2186  eqnetrrd  2288  neeqtrrd  2292  rspcedeq2vd  2745  dedhb  2798  eqsstr3d  3076  sseqtr4d  3078  syl6eqssr  3092  dfrab3ss  3293  uneqdifeqim  3387  ifbothdadc  3442  ifbothdc  3443  disjsn2  3525  diftpsn3  3600  dfopg  3642  unimax  3709  sndisj  3863  eqbrtrrd  3889  breqtrrd  3893  syl5breqr  3903  syl6eqbrr  3905  class2seteq  4019  opth1  4087  euotd  4105  opelopabsb  4111  tfisi  4430  0nelxp  4495  opeliunxp  4522  euiotaex  5030  iota4  5032  fun2ssres  5091  funimass1  5125  funssfv  5365  fnimapr  5399  fvun1  5405  fvco4  5411  elfvmptrab  5434  fmptco  5503  foima2  5569  foeqcnvco  5607  f1eqcocnv  5608  f1oiso2  5644  riotass2  5672  riotass  5673  f1ocnvfv3  5679  caovlem2d  5875  f1opw2  5888  sbcopeq1a  5995  csbopeq1a  5996  eloprabi  6004  cnvf1olem  6027  f2ndf  6029  smoiso  6105  nnaword  6310  eqer  6364  uniqs  6390  mapsncnv  6492  ixpiinm  6521  mapsnf1o  6534  ssenen  6647  findcard2  6685  findcard2s  6686  unsnfidcex  6710  fisseneq  6722  en1eqsn  6737  sbthlemi6  6751  updjud  6853  fodju0  6890  enq0sym  7088  enq0tr  7090  recexgt0sr  7416  caucvgsrlemoffcau  7440  axcaucvglemval  7529  le2tri3i  7690  cnegexlem2  7755  nnpcan  7802  addlsub  7945  negf1o  7957  subdi  7960  rereim  8160  cru  8176  divmulassap  8259  divmulasscomap  8260  divap1d  8365  div4p1lem1div2  8767  elz2  8916  zindd  8963  qapne  9223  divge1  9299  xrlttri3  9366  fseq1p1m1  9657  fzrevral  9668  nn0disj  9698  fzosplitsnm1  9769  fzosplitprm1  9794  flqlelt  9832  divfl0  9852  flqpmodeq  9883  zmodidfzo  9909  modqmuladd  9922  qnegmod  9925  addmodid  9928  modifeq2int  9942  modqeqmodmin  9950  modfzo0difsn  9951  modsumfzodifsn  9952  addmodlteq  9954  frecuzrdgsuc  9970  frecfzen2  9983  iseqf1olemab  10055  iseqf1olemmo  10058  ser3sub  10072  expgt1  10124  leexp2r  10140  sqoddm1div8  10237  bcm1k  10299  bcn2m1  10308  hashinfuni  10316  hashennnuni  10318  hashennn  10319  hashunlem  10343  hashprg  10347  fihashssdif  10357  zfz1isolem1  10376  shftlem  10381  shftfvalg  10383  shftfval  10386  replim  10424  cjexp  10458  resqrexlemcalc1  10578  resqrexlemcvg  10583  rersqrtthlem  10594  abssq  10645  recan  10673  negfi  10790  minclpr  10799  xrmaxiflemcom  10808  xrmineqinf  10828  xrminltinf  10831  xrminadd  10834  climmpt  10859  climrecl  10883  fsum3cvg  10936  summodclem3  10939  summodclem2a  10940  modfsummodlemstep  11016  isumsplit  11050  arisum  11057  geosergap  11065  geo2sum  11073  mertenslemi1  11094  mertenslem2  11095  efcj  11128  efsub  11136  eflegeo  11157  sinneg  11182  cosneg  11183  sin01bnd  11213  cos01bnd  11214  summodnegmod  11270  dvdseq  11292  addmodlteqALT  11303  mulmoddvds  11307  zob  11334  nn0ob  11351  divalgmod  11370  flodddiv4  11377  divgcdnnr  11410  gcdneg  11416  bezoutlemsup  11441  dvdssq  11463  lcmneg  11499  3lcm2e6woprm  11511  6lcm4e12  11512  divgcdcoprmex  11527  cncongr1  11528  cncongrcoprm  11531  oddpwdclemxy  11590  oddpwdclemodd  11593  divnumden  11617  zgcdsq  11622  phibnd  11636  hashgcdlem  11646  strndxid  11687  topnvalg  11832  toponcom  11893  tgtopon  11934  restopnb  12049  cnptoprest  12106  blfvalps  12187  bdmopn  12306  cnmet  12325