Theorem eqcomd 2143

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

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ext 2119

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

This theorem is referenced by:  eqtr2d  2171  eqtr3d  2172  eqtr4d  2173  syl5req  2183  syl6req  2187  sylan9req  2191  eqeltrrd  2215  eleqtrrd  2217  eleqtrrid  2227  eqeltrrdi  2229  eqnetrrd  2332  neeqtrrd  2336  rspcedeq2vd  2794  dedhb  2848  eqsstrrd  3129  sseqtrrd  3131  eqsstrrdi  3145  dfrab3ss  3349  uneqdifeqim  3443  ifbothdadc  3498  ifbothdc  3499  disjsn2  3581  diftpsn3  3656  dfopg  3698  unimax  3765  sndisj  3920  eqbrtrrd  3947  breqtrrd  3951  breqtrrid  3961  eqbrtrrdi  3963  class2seteq  4082  opth1  4153  euotd  4171  opelopabsb  4177  tfisi  4496  0nelxp  4562  opeliunxp  4589  euiotaex  5099  iota4  5101  fun2ssres  5161  funimass1  5195  funssfv  5440  fnimapr  5474  fvun1  5480  fvco4  5486  elfvmptrab  5509  fmptco  5579  foima2  5646  foeqcnvco  5684  f1eqcocnv  5685  f1oiso2  5721  riotass2  5749  riotass  5750  f1ocnvfv3  5756  caovlem2d  5956  f1opw2  5969  sbcopeq1a  6078  csbopeq1a  6079  eloprabi  6087  cnvf1olem  6114  f2ndf  6116  smoiso  6192  nnaword  6400  eqer  6454  uniqs  6480  mapsncnv  6582  ixpiinm  6611  mapsnf1o  6624  ssenen  6738  findcard2  6776  findcard2s  6777  unsnfidcex  6801  fisseneq  6813  phpeqd  6814  en1eqsn  6829  sbthlemi6  6843  updjud  6960  omp1eomlem  6972  fodju0  7012  enq0sym  7233  enq0tr  7235  recexgt0sr  7574  caucvgsrlemoffcau  7599  axcaucvglemval  7698  le2tri3i  7865  cnegexlem2  7931  nnpcan  7978  addlsub  8125  negf1o  8137  subdi  8140  rereim  8341  cru  8357  divmulassap  8448  divmulasscomap  8449  divap1d  8554  div4p1lem1div2  8966  elz2  9115  zindd  9162  qapne  9424  divge1  9503  xrlttri3  9576  fseq1p1m1  9867  fzrevral  9878  nn0disj  9908  fzosplitsnm1  9979  fzosplitprm1  10004  flqlelt  10042  divfl0  10062  flqpmodeq  10093  zmodidfzo  10119  modqmuladd  10132  qnegmod  10135  addmodid  10138  modifeq2int  10152  modqeqmodmin  10160  modfzo0difsn  10161  modsumfzodifsn  10162  addmodlteq  10164  frecuzrdgsuc  10180  frecfzen2  10193  iseqf1olemab  10255  iseqf1olemmo  10258  ser3sub  10272  expgt1  10324  leexp2r  10340  sqoddm1div8  10437  bcm1k  10499  bcn2m1  10508  hashinfuni  10516  hashennnuni  10518  hashennn  10519  hashunlem  10543  hashprg  10547  fihashssdif  10557  zfz1isolem1  10576  shftlem  10581  shftfvalg  10583  shftfval  10586  replim  10624  cjexp  10658  resqrexlemcalc1  10779  resqrexlemcvg  10784  rersqrtthlem  10795  abssq  10846  recan  10874  negfi  10992  minclpr  11001  xrmaxiflemcom  11011  xrmineqinf  11031  xrminltinf  11034  xrminadd  11037  climmpt  11062  climrecl  11086  fsum3cvg  11139  summodclem3  11142  summodclem2a  11143  modfsummodlemstep  11219  isumsplit  11253  arisum  11260  geosergap  11268  geo2sum  11276  mertenslemi1  11297  mertenslem2  11298  clim2divap  11302  fproddccvg  11334  efcj  11368  efsub  11376  eflegeo  11397  sinneg  11422  cosneg  11423  sin01bnd  11453  cos01bnd  11454  summodnegmod  11513  dvdseq  11535  addmodlteqALT  11546  mulmoddvds  11550  zob  11577  nn0ob  11594  divalgmod  11613  flodddiv4  11620  divgcdnnr  11653  gcdneg  11659  bezoutlemsup  11686  dvdssq  11708  lcmneg  11744  3lcm2e6woprm  11756  6lcm4e12  11757  divgcdcoprmex  11772  cncongr1  11773  cncongrcoprm  11776  oddpwdclemxy  11836  oddpwdclemodd  11839  divnumden  11863  zgcdsq  11868  phibnd  11882  hashgcdlem  11892  ennnfonelemex  11916  strndxid  11976  topnvalg  12121  toponcom  12183  tgtopon  12224  restopnb  12339  cnptoprest  12397  blfvalps  12543  bdmopn  12662  cnmet  12688  limcdifap  12789  dviaddf  12827  dvexp  12833  coseq0negpitopi  12906  abssinper  12916  subctctexmid  13185  cvgcmp2nlemabs  13216  trilpolemlt1  13223