Theorem eqcomd 2183

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

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  eqtr2d  2211  eqtr3d  2212  eqtr4d  2213  eqtr2id  2223  eqtr2di  2227  sylan9req  2231  eqeltrrd  2255  eleqtrrd  2257  eleqtrrid  2267  eqeltrrdi  2269  eqnetrrd  2373  neeqtrrd  2377  rspcedeq2vd  2852  dedhb  2907  eqsstrrd  3193  sseqtrrd  3195  eqsstrrdi  3209  dfrab3ss  3414  uneqdifeqim  3509  ifbothdadc  3567  ifbothdc  3568  disjsn2  3656  diftpsn3  3734  dfopg  3777  unimax  3844  sndisj  4000  eqbrtrrd  4028  breqtrrd  4032  breqtrrid  4042  eqbrtrrdi  4044  class2seteq  4164  opth1  4237  euotd  4255  opelopabsb  4261  tfisi  4587  0nelxp  4655  opeliunxp  4682  euiotaex  5195  iota4  5197  iotam  5209  fun2ssres  5260  funimass1  5294  funssfv  5542  fnimapr  5577  fvun1  5583  fvco4  5589  elfvmptrab  5612  fmptco  5683  foima2  5753  foeqcnvco  5791  f1eqcocnv  5792  f1oiso2  5828  riotass2  5857  riotass  5858  f1ocnvfv3  5864  caovlem2d  6067  f1opw2  6077  sbcopeq1a  6188  csbopeq1a  6189  eloprabi  6197  cnvf1olem  6225  f2ndf  6227  smoiso  6303  nnaword  6512  eqer  6567  uniqs  6593  mapsncnv  6695  ixpiinm  6724  mapsnf1o  6737  ssenen  6851  findcard2  6889  findcard2s  6890  unsnfidcex  6919  fisseneq  6931  phpeqd  6932  en1eqsn  6947  sbthlemi6  6961  updjud  7081  omp1eomlem  7093  nnnninf2  7125  nninfisollem0  7128  nninfisollemeq  7130  fodju0  7145  3nsssucpw1  7235  enq0sym  7431  enq0tr  7433  recexgt0sr  7772  caucvgsrlemoffcau  7797  axcaucvglemval  7896  le2tri3i  8066  cnegexlem2  8133  nnpcan  8180  addlsub  8327  negf1o  8339  subdi  8342  rereim  8543  cru  8559  divmulassap  8652  divmulasscomap  8653  divap1d  8758  div4p1lem1div2  9172  difgtsumgt  9322  elz2  9324  zindd  9371  qapne  9639  divge1  9723  xrlttri3  9797  fseq1p1m1  10094  fzrevral  10105  nn0disj  10138  fzosplitsnm1  10209  fzosplitprm1  10234  flqlelt  10276  divfl0  10296  flqpmodeq  10327  zmodidfzo  10353  modqmuladd  10366  qnegmod  10369  addmodid  10372  modifeq2int  10386  modqeqmodmin  10394  modfzo0difsn  10395  modsumfzodifsn  10396  addmodlteq  10398  frecuzrdgsuc  10414  frecfzen2  10427  iseqf1olemab  10489  iseqf1olemmo  10492  ser3sub  10506  expgt1  10558  leexp2r  10574  sqoddm1div8  10674  mulsubdivbinom2ap  10691  bcm1k  10740  bcn2m1  10749  hashinfuni  10757  hashennnuni  10759  hashennn  10760  hashunlem  10784  hashprg  10788  fihashssdif  10798  zfz1isolem1  10820  shftlem  10825  shftfvalg  10827  shftfval  10830  replim  10868  cjexp  10902  resqrexlemcalc1  11023  resqrexlemcvg  11028  rersqrtthlem  11039  abssq  11090  recan  11118  negfi  11236  minclpr  11245  mingeb  11250  xrmaxiflemcom  11257  xrmineqinf  11277  xrminltinf  11280  xrminadd  11283  climmpt  11308  climrecl  11332  fsum3cvg  11386  summodclem3  11388  summodclem2a  11389  modfsummodlemstep  11465  isumsplit  11499  arisum  11506  geosergap  11514  geo2sum  11522  mertenslemi1  11543  mertenslem2  11544  clim2divap  11548  fproddccvg  11580  fprodssdc  11598  fprodabs  11624  fproddivapf  11639  fprodmodd  11649  efcj  11681  efsub  11689  eflegeo  11709  sinneg  11734  cosneg  11735  sin01bnd  11765  cos01bnd  11766  modm1div  11807  summodnegmod  11829  dvdseq  11854  addmodlteqALT  11865  mulmoddvds  11869  zob  11896  nn0ob  11913  divalgmod  11932  flodddiv4  11939  divgcdnnr  11977  gcdneg  11983  bezoutlemsup  12010  dvdssq  12032  lcmneg  12074  3lcm2e6woprm  12086  6lcm4e12  12087  divgcdcoprmex  12102  cncongr1  12103  cncongrcoprm  12106  oddpwdclemxy  12169  oddpwdclemodd  12172  divnumden  12196  zgcdsq  12201  phibnd  12217  hashgcdlem  12238  vfermltl  12251  powm2modprm  12252  reumodprminv  12253  pythagtriplem19  12282  pcprendvds2  12291  pczpre  12297  dvdsprmpweqle  12336  difsqpwdvds  12337  4sqlem4  12390  ennnfonelemex  12415  strndxid  12490  topnvalg  12700  intopsn  12786  ismgmid2  12799  mgmidsssn0  12803  mndpfo  12839  mndfo  12840  mndinvmod  12846  mnd1id  12848  mhmf1o  12861  0mhm  12873  grpidd2  12914  grpinvid2  12925  grpidssd  12946  grpnpcan  12962  grpsubsub4  12963  mulginvcom  13008  grpissubg  13054  mgpress  13141  srg1zr  13170  srgmulgass  13172  srgpcomp  13173  srgpcomppsc  13175  ringadd2  13210  ringo2times  13211  ringlz  13222  ringrz  13223  ringinvnzdiv  13227  ringnegl  13228  ringnegr  13229  crngunit  13280  lringuplu  13337  lmod0vs  13411  lmodvsmmulgdi  13413  lmodfopne  13416  zringinvg  13497  toponcom  13530  tgtopon  13569  restopnb  13684  cnptoprest  13742  blfvalps  13888  bdmopn  14007  cnmet  14033  limcdifap  14134  dviaddf  14172  dvexp  14178  coseq0negpitopi  14260  abssinper  14270  rplogbzexp  14375  lgsvalmod  14423  lgsneg  14428  subctctexmid  14753  cvgcmp2nlemabs  14783  trilpolemlt1  14792