Theorem eqcomd 2171

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

Syntax hints:   -> wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-ext 2147

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

This theorem is referenced by:  eqtr2d  2199  eqtr3d  2200  eqtr4d  2201  eqtr2id  2211  eqtr2di  2215  sylan9req  2219  eqeltrrd  2243  eleqtrrd  2245  eleqtrrid  2255  eqeltrrdi  2257  eqnetrrd  2361  neeqtrrd  2365  rspcedeq2vd  2839  dedhb  2894  eqsstrrd  3178  sseqtrrd  3180  eqsstrrdi  3194  dfrab3ss  3399  uneqdifeqim  3493  ifbothdadc  3550  ifbothdc  3551  disjsn2  3638  diftpsn3  3713  dfopg  3755  unimax  3822  sndisj  3977  eqbrtrrd  4005  breqtrrd  4009  breqtrrid  4019  eqbrtrrdi  4021  class2seteq  4141  opth1  4213  euotd  4231  opelopabsb  4237  tfisi  4563  0nelxp  4631  opeliunxp  4658  euiotaex  5168  iota4  5170  fun2ssres  5230  funimass1  5264  funssfv  5511  fnimapr  5545  fvun1  5551  fvco4  5557  elfvmptrab  5580  fmptco  5650  foima2  5719  foeqcnvco  5757  f1eqcocnv  5758  f1oiso2  5794  riotass2  5823  riotass  5824  f1ocnvfv3  5830  caovlem2d  6030  f1opw2  6043  sbcopeq1a  6152  csbopeq1a  6153  eloprabi  6161  cnvf1olem  6188  f2ndf  6190  smoiso  6266  nnaword  6475  eqer  6529  uniqs  6555  mapsncnv  6657  ixpiinm  6686  mapsnf1o  6699  ssenen  6813  findcard2  6851  findcard2s  6852  unsnfidcex  6881  fisseneq  6893  phpeqd  6894  en1eqsn  6909  sbthlemi6  6923  updjud  7043  omp1eomlem  7055  nnnninf2  7087  nninfisollem0  7090  nninfisollemeq  7092  fodju0  7107  3nsssucpw1  7188  enq0sym  7369  enq0tr  7371  recexgt0sr  7710  caucvgsrlemoffcau  7735  axcaucvglemval  7834  le2tri3i  8003  cnegexlem2  8070  nnpcan  8117  addlsub  8264  negf1o  8276  subdi  8279  rereim  8480  cru  8496  divmulassap  8587  divmulasscomap  8588  divap1d  8693  div4p1lem1div2  9106  difgtsumgt  9256  elz2  9258  zindd  9305  qapne  9573  divge1  9655  xrlttri3  9729  fseq1p1m1  10025  fzrevral  10036  nn0disj  10069  fzosplitsnm1  10140  fzosplitprm1  10165  flqlelt  10207  divfl0  10227  flqpmodeq  10258  zmodidfzo  10284  modqmuladd  10297  qnegmod  10300  addmodid  10303  modifeq2int  10317  modqeqmodmin  10325  modfzo0difsn  10326  modsumfzodifsn  10327  addmodlteq  10329  frecuzrdgsuc  10345  frecfzen2  10358  iseqf1olemab  10420  iseqf1olemmo  10423  ser3sub  10437  expgt1  10489  leexp2r  10505  sqoddm1div8  10604  bcm1k  10669  bcn2m1  10678  hashinfuni  10686  hashennnuni  10688  hashennn  10689  hashunlem  10713  hashprg  10717  fihashssdif  10727  zfz1isolem1  10749  shftlem  10754  shftfvalg  10756  shftfval  10759  replim  10797  cjexp  10831  resqrexlemcalc1  10952  resqrexlemcvg  10957  rersqrtthlem  10968  abssq  11019  recan  11047  negfi  11165  minclpr  11174  mingeb  11179  xrmaxiflemcom  11186  xrmineqinf  11206  xrminltinf  11209  xrminadd  11212  climmpt  11237  climrecl  11261  fsum3cvg  11315  summodclem3  11317  summodclem2a  11318  modfsummodlemstep  11394  isumsplit  11428  arisum  11435  geosergap  11443  geo2sum  11451  mertenslemi1  11472  mertenslem2  11473  clim2divap  11477  fproddccvg  11509  fprodssdc  11527  fprodabs  11553  fproddivapf  11568  fprodmodd  11578  efcj  11610  efsub  11618  eflegeo  11638  sinneg  11663  cosneg  11664  sin01bnd  11694  cos01bnd  11695  modm1div  11736  summodnegmod  11758  dvdseq  11782  addmodlteqALT  11793  mulmoddvds  11797  zob  11824  nn0ob  11841  divalgmod  11860  flodddiv4  11867  divgcdnnr  11905  gcdneg  11911  bezoutlemsup  11938  dvdssq  11960  lcmneg  12002  3lcm2e6woprm  12014  6lcm4e12  12015  divgcdcoprmex  12030  cncongr1  12031  cncongrcoprm  12034  oddpwdclemxy  12097  oddpwdclemodd  12100  divnumden  12124  zgcdsq  12129  phibnd  12145  hashgcdlem  12166  vfermltl  12179  powm2modprm  12180  reumodprminv  12181  pythagtriplem19  12210  pcprendvds2  12219  pczpre  12225  dvdsprmpweqle  12264  difsqpwdvds  12265  4sqlem4  12318  ennnfonelemex  12343  strndxid  12418  topnvalg  12563  toponcom  12625  tgtopon  12666  restopnb  12781  cnptoprest  12839  blfvalps  12985  bdmopn  13104  cnmet  13130  limcdifap  13231  dviaddf  13269  dvexp  13275  coseq0negpitopi  13357  abssinper  13367  rplogbzexp  13472  lgsvalmod  13520  lgsneg  13525  subctctexmid  13841  cvgcmp2nlemabs  13871  trilpolemlt1  13880