Theorem eqcomd 2199

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 2195	. 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 1458  ax-gen 1460  ax-ext 2175

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

This theorem is referenced by:  eqtr2d  2227  eqtr3d  2228  eqtr4d  2229  eqtr2id  2239  eqtr2di  2243  sylan9req  2247  eqeltrrd  2271  eleqtrrd  2273  eleqtrrid  2283  eqeltrrdi  2285  eqnetrrd  2390  neeqtrrd  2394  rspcedeq2vd  2874  dedhb  2929  eqsstrrd  3216  sseqtrrd  3218  eqsstrrdi  3232  dfrab3ss  3437  uneqdifeqim  3532  ifbothdadc  3589  ifbothdc  3590  disjsn2  3681  diftpsn3  3759  dfopg  3802  unimax  3869  sndisj  4025  eqbrtrrd  4053  breqtrrd  4057  breqtrrid  4067  eqbrtrrdi  4069  class2seteq  4192  opth1  4265  euotd  4283  opelopabsb  4290  tfisi  4619  0nelxp  4687  opeliunxp  4714  euiotaex  5231  iota4  5234  iotam  5246  fun2ssres  5297  funimass1  5331  funssfv  5580  fnimapr  5617  fvun1  5623  fvco4  5629  elfvmptrab  5653  fmptco  5724  foima2  5794  foeqcnvco  5833  f1eqcocnv  5834  f1oiso2  5870  riotass2  5900  riotass  5901  f1ocnvfv3  5907  caovlem2d  6111  f1opw2  6124  sbcopeq1a  6240  csbopeq1a  6241  eloprabi  6249  cnvf1olem  6277  f2ndf  6279  smoiso  6355  nnaword  6564  eqer  6619  uniqs  6647  mapsncnv  6749  ixpiinm  6778  mapsnf1o  6791  ssenen  6907  findcard2  6945  findcard2s  6946  unsnfidcex  6976  fisseneq  6988  phpeqd  6989  en1eqsn  7007  sbthlemi6  7021  updjud  7141  omp1eomlem  7153  nnnninf2  7186  nninfisollem0  7189  nninfisollemeq  7191  fodju0  7206  3nsssucpw1  7296  enq0sym  7492  enq0tr  7494  recexgt0sr  7833  caucvgsrlemoffcau  7858  axcaucvglemval  7957  le2tri3i  8128  cnegexlem2  8195  nnpcan  8242  addlsub  8389  negf1o  8401  subdi  8404  rereim  8605  cru  8621  divmulassap  8714  divmulasscomap  8715  divap1d  8820  subhalfhalf  9217  div4p1lem1div2  9236  difgtsumgt  9386  elz2  9388  zindd  9435  qapne  9704  divge1  9789  xrlttri3  9863  fseq1p1m1  10160  fzrevral  10171  nn0disj  10204  fzosplitsnm1  10276  fzosplitprm1  10301  flqlelt  10345  divfl0  10365  flqpmodeq  10398  zmodidfzo  10424  modqmuladd  10437  qnegmod  10440  addmodid  10443  modifeq2int  10457  modqeqmodmin  10465  modfzo0difsn  10466  modsumfzodifsn  10467  addmodlteq  10469  frecuzrdgsuc  10485  frecfzen2  10498  iseqf1olemab  10573  iseqf1olemmo  10576  seqf1oglem1  10590  seqf1oglem2  10591  ser3sub  10594  expgt1  10648  leexp2r  10664  sqoddm1div8  10764  mulsubdivbinom2ap  10782  bcm1k  10831  bcn2m1  10840  hashinfuni  10848  hashennnuni  10850  hashennn  10851  hashunlem  10875  hashprg  10879  fihashssdif  10889  zfz1isolem1  10911  elovmpowrd  10955  shftlem  10960  shftfvalg  10962  shftfval  10965  replim  11003  cjexp  11037  resqrexlemcalc1  11158  resqrexlemcvg  11163  rersqrtthlem  11174  abssq  11225  recan  11253  negfi  11371  minclpr  11380  mingeb  11385  xrmaxiflemcom  11392  xrmineqinf  11412  xrminltinf  11415  xrminadd  11418  climmpt  11443  climrecl  11467  fsum3cvg  11521  summodclem3  11523  summodclem2a  11524  modfsummodlemstep  11600  isumsplit  11634  arisum  11641  geosergap  11649  geo2sum  11657  mertenslemi1  11678  mertenslem2  11679  clim2divap  11683  fproddccvg  11715  fprodssdc  11733  fprodabs  11759  fproddivapf  11774  fprodmodd  11784  efcj  11816  efsub  11824  eflegeo  11844  sinneg  11869  cosneg  11870  sin01bnd  11900  cos01bnd  11901  modm1div  11943  summodnegmod  11965  dvdseq  11990  addmodlteqALT  12001  mulmoddvds  12005  zob  12032  nn0ob  12049  divalgmod  12068  flodddiv4  12075  divgcdnnr  12113  gcdneg  12119  bezoutlemsup  12146  dvdssq  12168  lcmneg  12212  3lcm2e6woprm  12224  6lcm4e12  12225  divgcdcoprmex  12240  cncongr1  12241  cncongrcoprm  12244  oddpwdclemxy  12307  oddpwdclemodd  12310  divnumden  12334  zgcdsq  12339  phibnd  12355  hashgcdlem  12376  vfermltl  12389  powm2modprm  12390  reumodprminv  12391  pythagtriplem19  12420  pcprendvds2  12429  pczpre  12435  dvdsprmpweqle  12475  difsqpwdvds  12476  4sqlem4  12530  ennnfonelemex  12571  strndxid  12646  topnvalg  12862  intopsn  12950  ismgmid2  12963  mgmidsssn0  12967  gsumfzval  12974  gsumprval  12982  mndpfo  13019  mndfo  13020  mndinvmod  13026  mnd1id  13028  mhmf1o  13042  0mhm  13058  gsumwmhm  13070  grpidd2  13113  grpinvid2  13125  grpidssd  13148  grpnpcan  13164  grpsubsub4  13165  qusgrp2  13183  mulginvcom  13217  grpissubg  13264  quselbasg  13300  qus0  13305  ecqusaddd  13308  ghmid  13319  ghminv  13320  imasabl  13406  gsumfzmhm  13413  mgpress  13427  rnglz  13441  rngrz  13442  rngmneg1  13443  rngmneg2  13444  rngpropd  13451  srg1zr  13483  srgmulgass  13485  srgpcomp  13486  srgpcomppsc  13488  ringadd2  13523  ringo2times  13524  ringlz  13539  ringrz  13540  ringinvnzdiv  13546  ringnegl  13547  ringnegr  13548  imasring  13560  qusring2  13562  crngunit  13607  rhmopp  13672  lringuplu  13692  opprdomnbg  13770  lmod0vs  13817  lmodvsmmulgdi  13819  lmodfopne  13822  islss3  13875  lspsn  13912  lmodindp1  13924  rnglidlmmgm  13992  rnglidlmsgrp  13993  rnglidlrng  13994  isridl  14000  zringinvg  14092  zndvds  14137  znf1o  14139  toponcom  14195  tgtopon  14234  restopnb  14349  cnptoprest  14407  blfvalps  14553  bdmopn  14672  cnmet  14698  limcdifap  14816  dviaddf  14854  dvexp  14860  coseq0negpitopi  14971  abssinper  14981  rplogbzexp  15086  lgsvalmod  15135  lgsneg  15140  gausslemma2dlem1a  15174  gausslemma2dlem6  15183  gausslemma2dlem7  15184  gausslemma2d  15185  subctctexmid  15491  cvgcmp2nlemabs  15522  trilpolemlt1  15531