Theorem eqcomd 2202

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-ext 2178

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

This theorem is referenced by:  eqtr2d  2230  eqtr3d  2231  eqtr4d  2232  eqtr2id  2242  eqtr2di  2246  sylan9req  2250  eqeltrrd  2274  eleqtrrd  2276  eleqtrrid  2286  eqeltrrdi  2288  eqnetrrd  2393  neeqtrrd  2397  rspcedeq2vd  2878  dedhb  2933  eqsstrrd  3221  sseqtrrd  3223  eqsstrrdi  3237  dfrab3ss  3442  uneqdifeqim  3537  ifbothdadc  3594  ifbothdc  3595  disjsn2  3686  diftpsn3  3764  dfopg  3807  unimax  3874  sndisj  4030  eqbrtrrd  4058  breqtrrd  4062  breqtrrid  4072  eqbrtrrdi  4074  class2seteq  4197  opth1  4270  euotd  4288  opelopabsb  4295  tfisi  4624  0nelxp  4692  opeliunxp  4719  euiotaex  5236  iota4  5239  iotam  5251  fun2ssres  5302  funimass1  5336  funssfv  5587  fnimapr  5624  fvun1  5630  fvco4  5636  elfvmptrab  5660  fmptco  5731  foima2  5801  foeqcnvco  5840  f1eqcocnv  5841  f1oiso2  5877  riotass2  5907  riotass  5908  f1ocnvfv3  5914  fvmpopr2d  6063  caovlem2d  6120  f1opw2  6133  offveq  6160  sbcopeq1a  6254  csbopeq1a  6255  eloprabi  6263  cnvf1olem  6291  f2ndf  6293  smoiso  6369  nnaword  6578  eqer  6633  uniqs  6661  mapsncnv  6763  ixpiinm  6792  mapsnf1o  6805  ssenen  6921  findcard2  6959  findcard2s  6960  unsnfidcex  6990  fisseneq  7004  phpeqd  7005  en1eqsn  7023  sbthlemi6  7037  updjud  7157  omp1eomlem  7169  nnnninf2  7202  nninfisollem0  7205  nninfisollemeq  7207  fodju0  7222  3nsssucpw1  7319  enq0sym  7516  enq0tr  7518  recexgt0sr  7857  caucvgsrlemoffcau  7882  axcaucvglemval  7981  le2tri3i  8152  cnegexlem2  8219  nnpcan  8266  addlsub  8413  negf1o  8425  subdi  8428  rereim  8630  cru  8646  divmulassap  8739  divmulasscomap  8740  divap1d  8845  subhalfhalf  9243  div4p1lem1div2  9262  difgtsumgt  9412  elz2  9414  zindd  9461  qapne  9730  divge1  9815  xrlttri3  9889  fseq1p1m1  10186  fzrevral  10197  nn0disj  10230  fzosplitsnm1  10302  fzosplitprm1  10327  flqlelt  10383  divfl0  10403  flqpmodeq  10436  zmodidfzo  10462  modqmuladd  10475  qnegmod  10478  addmodid  10481  modifeq2int  10495  modqeqmodmin  10503  modfzo0difsn  10504  modsumfzodifsn  10505  addmodlteq  10507  frecuzrdgsuc  10523  frecfzen2  10536  iseqf1olemab  10611  iseqf1olemmo  10614  seqf1oglem1  10628  seqf1oglem2  10629  ser3sub  10632  expgt1  10686  leexp2r  10702  sqoddm1div8  10802  mulsubdivbinom2ap  10820  bcm1k  10869  bcn2m1  10878  hashinfuni  10886  hashennnuni  10888  hashennn  10889  hashunlem  10913  hashprg  10917  fihashssdif  10927  zfz1isolem1  10949  elovmpowrd  10993  shftlem  10998  shftfvalg  11000  shftfval  11003  replim  11041  cjexp  11075  resqrexlemcalc1  11196  resqrexlemcvg  11201  rersqrtthlem  11212  abssq  11263  recan  11291  negfi  11410  minclpr  11419  mingeb  11424  xrmaxiflemcom  11431  xrmineqinf  11451  xrminltinf  11454  xrminadd  11457  climmpt  11482  climrecl  11506  fsum3cvg  11560  summodclem3  11562  summodclem2a  11563  modfsummodlemstep  11639  isumsplit  11673  arisum  11680  geosergap  11688  geo2sum  11696  mertenslemi1  11717  mertenslem2  11718  clim2divap  11722  fproddccvg  11754  fprodssdc  11772  fprodabs  11798  fproddivapf  11813  fprodmodd  11823  efcj  11855  efsub  11863  eflegeo  11883  sinneg  11908  cosneg  11909  sin01bnd  11939  cos01bnd  11940  modm1div  11982  summodnegmod  12004  dvdseq  12030  addmodlteqALT  12041  mulmoddvds  12045  zob  12073  nn0ob  12090  divalgmod  12109  flodddiv4  12118  bitsinv1  12144  divgcdnnr  12168  gcdneg  12174  bezoutlemsup  12201  dvdssq  12223  lcmneg  12267  3lcm2e6woprm  12279  6lcm4e12  12280  divgcdcoprmex  12295  cncongr1  12296  cncongrcoprm  12299  oddpwdclemxy  12362  oddpwdclemodd  12365  divnumden  12389  zgcdsq  12394  phibnd  12410  hashgcdlem  12431  vfermltl  12445  powm2modprm  12446  reumodprminv  12447  pythagtriplem19  12476  pcprendvds2  12485  pczpre  12491  dvdsprmpweqle  12531  difsqpwdvds  12532  4sqlem4  12586  ennnfonelemex  12656  strndxid  12731  topnvalg  12953  prdssca  12977  intopsn  13069  ismgmid2  13082  mgmidsssn0  13086  gsumfzval  13093  gsumprval  13101  mndpfo  13140  mndfo  13141  mndinvmod  13147  prds0g  13151  mnd1id  13158  mhmf1o  13172  0mhm  13188  gsumwmhm  13200  grpidd2  13243  grpinvid2  13255  grpidssd  13278  grpnpcan  13294  grpsubsub4  13295  qusgrp2  13319  mulginvcom  13353  grpissubg  13400  quselbasg  13436  qus0  13441  ecqusaddd  13444  ghmid  13455  ghminv  13456  imasabl  13542  gsumfzmhm  13549  mgpress  13563  rnglz  13577  rngrz  13578  rngmneg1  13579  rngmneg2  13580  rngpropd  13587  srg1zr  13619  srgmulgass  13621  srgpcomp  13622  srgpcomppsc  13624  ringadd2  13659  ringo2times  13660  ringlz  13675  ringrz  13676  ringinvnzdiv  13682  ringnegl  13683  ringnegr  13684  imasring  13696  qusring2  13698  crngunit  13743  rhmopp  13808  lringuplu  13828  opprdomnbg  13906  lmod0vs  13953  lmodvsmmulgdi  13955  lmodfopne  13958  islss3  14011  lspsn  14048  lmodindp1  14060  rnglidlmmgm  14128  rnglidlmsgrp  14129  rnglidlrng  14130  isridl  14136  zringinvg  14236  zndvds  14281  znf1o  14283  psrgrp  14313  toponcom  14347  tgtopon  14386  restopnb  14501  cnptoprest  14559  blfvalps  14705  bdmopn  14824  cnmet  14850  mpomulcn  14886  limcdifap  14982  dvidsslem  15013  dviaddf  15025  dvexp  15031  dvply2g  15086  coseq0negpitopi  15156  abssinper  15166  rplogbzexp  15274  dvdsppwf1o  15309  mpodvdsmulf1o  15310  fsumdvdsmul  15311  sgmmul  15316  perfect  15321  lgsvalmod  15344  lgsneg  15349  gausslemma2dlem1a  15383  gausslemma2dlem6  15392  gausslemma2dlem7  15393  gausslemma2d  15394  lgsquadlem2  15403  2lgslem1a1  15411  2lgslem1a  15413  2lgslem3c  15420  2lgslem3d  15421  2lgslem3d1  15425  2lgs  15429  2lgsoddprm  15438  subctctexmid  15731  cvgcmp2nlemabs  15763  trilpolemlt1  15772