Theorem eqcomd 2244

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

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-ext 2220

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

This theorem is referenced by:  eqtr2d  2272  eqtr3d  2273  eqtr4d  2274  eqtr2id  2284  eqtr2di  2288  sylan9req  2292  eqeltrrd  2316  eleqtrrd  2318  eleqtrrid  2328  eqeltrrdi  2330  eqabcdv  2370  eqnetrrd  2446  neeqtrrd  2450  rspcedeq2vd  2940  dedhb  2995  eqsstrrd  3285  sseqtrrd  3287  eqsstrrdi  3301  dfrab3ss  3511  uneqdifeqim  3610  ifbothdadc  3671  ifbothdc  3672  2if2dc  3677  ifeqeqxdc  3684  disjsn2  3768  diftpsn3  3851  elpr2elpr  3896  dfopg  3897  unimax  3964  sndisj  4121  eqbrtrrd  4149  breqtrrd  4153  breqtrrid  4163  eqbrtrrdi  4165  class2seteq  4295  opth1  4371  euotd  4390  opelopabsb  4397  tfisi  4729  0nelxp  4797  opeliunxp  4825  euiotaex  5349  iota4  5352  iotam  5364  fun2ssres  5416  funimass1  5453  funssfv  5716  fnimapr  5757  fvun1  5763  fvco4  5771  elfvmptrab  5795  fmptco  5865  fncofn  5884  foima2  5947  foeqcnvco  5986  f1eqcocnv  5987  f1oiso2  6023  riotass2  6057  riotass  6058  f1ocnvfv3  6064  fvmpopr2d  6215  caovlem2d  6272  f1opw2  6286  offveq  6313  sbcopeq1a  6411  csbopeq1a  6412  eloprabi  6422  cnvf1olem  6450  f2ndf  6452  suppval1  6469  suppsnopdc  6480  smoiso  6563  nnaword  6774  eqer  6829  uniqs  6857  mapsncnv  6967  ixpiinm  6996  mapsnf1o  7009  mapunen  7141  ssenen  7142  findcard2  7183  findcard2s  7184  unsnfidcex  7217  fisseneq  7232  phpeqd  7233  en1eqsn  7255  sbthlemi6  7269  updjud  7412  omp1eomlem  7424  nnnninf2  7457  nninfisollem0  7460  nninfisollemeq  7462  fodju0  7477  3nsssucpw1  7585  enq0sym  7789  enq0tr  7791  recexgt0sr  8130  caucvgsrlemoffcau  8155  axcaucvglemval  8254  le2tri3i  8424  cnegexlem2  8492  nnpcan  8539  addlsub  8686  negf1o  8699  subdi  8702  rereim  8904  cru  8920  divmulassap  9015  divmulasscomap  9016  divap1d  9121  subhalfhalf  9519  div4p1lem1div2  9538  difgtsumgt  9693  elz2  9695  zindd  9743  qapne  10018  divge1  10103  xrlttri3  10178  fseq1p1m1  10479  fzrevral  10490  nn0disj  10523  fzo0addel  10584  fzosplitsnm1  10605  fzosplitprm1  10631  flqlelt  10689  divfl0  10709  flqpmodeq  10742  zmodidfzo  10768  modqmuladd  10781  qnegmod  10784  addmodid  10787  modifeq2int  10801  modqeqmodmin  10809  modfzo0difsn  10810  modsumfzodifsn  10811  addmodlteq  10813  frecuzrdgsuc  10829  frecfzen2  10842  iseqf1olemab  10917  iseqf1olemmo  10920  seqf1oglem1  10934  seqf1oglem2  10935  ser3sub  10938  expgt1  10992  leexp2r  11008  sqoddm1div8  11109  mulsubdivbinom2ap  11127  bcm1k  11176  bcn2m1  11186  hashinfuni  11194  hashennnuni  11196  hashennn  11197  hashunlem  11222  hashprg  11227  fihashssdif  11237  hashfibclem  11260  hashfibc  11261  hashf1lem1  11263  hashf1lem2  11264  zfz1isolem1  11270  elovmpowrd  11324  ccatsymb  11348  ccatlid  11352  eqs1  11374  ccatw2s1p1g  11391  swrdfv2  11413  swrds1  11418  swrdlsw  11419  pfxfv  11434  swrdswrd  11455  swrdpfx  11457  pfxpfx  11458  pfxlswccat  11463  ccats1pfxeq  11464  wrdind  11472  wrd2ind  11473  pfxccatin12lem1  11478  pfxccatin12lem2  11481  swrdccat3blem  11489  swrdccat3b  11490  ccats1pfxeqbi  11492  reuccatpfxs1lem  11496  reuccatpfxs1  11497  s3s4d  11553  s2s5d  11554  s5s2d  11555  shftlem  11559  shftfvalg  11561  shftfval  11564  replim  11602  cjexp  11636  sq01  11638  resqrexlemcalc1  11758  resqrexlemcvg  11763  rersqrtthlem  11774  abssq  11825  recan  11853  negfi  11972  minclpr  11981  mingeb  11986  xrmaxiflemcom  11993  xrmineqinf  12013  xrminltinf  12016  xrminadd  12019  climmpt  12044  climrecl  12068  fsum3cvg  12123  summodclem3  12125  summodclem2a  12126  modfsummodlemstep  12202  isumsplit  12236  arisum  12243  geosergap  12251  geo2sum  12259  mertenslemi1  12280  mertenslem2  12281  clim2divap  12285  fproddccvg  12317  fprodssdc  12335  fprodabs  12361  fproddivapf  12376  fprodmodd  12386  efcj  12418  efsub  12426  eflegeo  12446  sinneg  12471  cosneg  12472  sin01bnd  12502  cos01bnd  12503  modm1div  12545  summodnegmod  12567  dvdseq  12593  addmodlteqALT  12604  mulmoddvds  12608  zob  12636  nn0ob  12653  divalgmod  12672  flodddiv4  12681  bitsinv1  12707  divgcdnnr  12731  gcdneg  12737  bezoutlemsup  12764  dvdssq  12786  lcmneg  12830  3lcm2e6woprm  12842  6lcm4e12  12843  divgcdcoprmex  12858  cncongr1  12859  cncongrcoprm  12862  oddpwdclemxy  12925  oddpwdclemodd  12928  divnumden  12952  zgcdsq  12957  phibnd  12973  hashgcdlem  12994  vfermltl  13008  powm2modprm  13009  reumodprminv  13010  pythagtriplem19  13039  pcprendvds2  13048  pczpre  13054  dvdsprmpweqle  13094  difsqpwdvds  13095  4sqlem4  13149  ballotfilemfp1  13209  ballotfilemsf1o  13235  ballotfilemrinv0  13254  ennnfonelemex  13283  strndxid  13358  topnvalg  13582  intopsn  13664  ismgmid2  13677  mgmidsssn0  13681  gzsumfzval  13688  mndpfo  13728  mndfo  13729  mndinvmod  13735  mnd1id  13740  mhmf1o  13754  0mhm  13770  gzsumwmhm  13780  grpidd2  13823  grpinvid2  13835  grpidssd  13858  grpnpcan  13874  grpsubsub4  13875  qusgrp2  13893  mulginvcom  13927  grpissubg  13974  quselbasg  14010  qus0  14015  ecqusaddd  14018  ghmid  14029  ghminv  14030  imasabl  14117  gzsummhm  14122  gzsumsplit0  14125  gzsumshift  14126  gsumsncmn  14133  prdssca  14152  prds0g  14172  mgpress  14205  rnglz  14219  rngrz  14220  rngmneg1  14221  rngmneg2  14222  rngpropd  14229  rng1zrlem  14233  srgmulgass  14267  srgpcomp  14268  srgpcomppsc  14270  ringadd2  14305  ringo2times  14306  ringlz  14321  ringrz  14322  ringinvnzdiv  14328  ringnegl  14329  ringnegr  14330  imasring  14342  qusring2  14344  crngunit  14391  rhmopp  14456  lringuplu  14476  opprdomnbg  14556  lmod0vs  14630  lmodvsmmulgdi  14632  lmodfopne  14635  islss3  14688  lspsn  14725  lmodindp1  14737  rnglidlmmgm  14805  rnglidlmsgrp  14806  rnglidlrng  14807  isridl  14813  zringinvg  14911  zndvds  14956  znf1o  14958  psrgrp  14999  toponcom  15051  tgtopon  15090  restopnb  15205  cnptoprest  15263  blfvalps  15409  bdmopn  15528  cnmet  15554  mpomulcn  15590  limcdifap  15686  dvidsslem  15717  dviaddf  15729  dvexp  15735  dvply2g  15790  coseq0negpitopi  15860  abssinper  15870  rplogbzexp  15979  pellexlem2  16006  dvdsppwf1o  16017  mpodvdsmulf1o  16018  fsumdvdsmul  16019  sgmmul  16024  perfect  16029  lgsvalmod  16052  lgsneg  16057  gausslemma2dlem1a  16091  gausslemma2dlem6  16100  gausslemma2dlem7  16101  gausslemma2d  16102  lgsquadlem2  16111  2lgslem1a1  16119  2lgslem1a  16121  2lgslem3c  16128  2lgslem3d  16129  2lgslem3d1  16133  2lgs  16137  2lgsoddprm  16146  uhgrun  16241  upgrun  16281  umgrun  16283  ushgredgedg  16381  issubgr2  16413  uhgrissubgr  16416  subgruhgredgdm  16425  subumgredg2en  16426  subupgr  16428  p1evtxdeqfilem  16466  wlklenvm1  16496  wlklenvm1g  16497  wlkl1loop  16513  upgriswlkdc  16515  uspgr2wlkeq  16520  uspgr2wlkeq2  16521  uspgr2wlkeqi  16522  wlkres  16534  loopclwwlkn1b  16574  clwwlkn1loopb  16575  clwwlkext2edg  16577  clwwlknonccat  16588  s2elclwwlknon2  16591  clwwlknonex2lem2  16593  clwwlknun  16596  eupth2lem3fi  16631  eupth2lembfi  16632  subctctexmid  16944  cvgcmp2nlemabs  16986  trilpolemlt1  16995