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 )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used 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  3613  ifbothdadc  3674  ifbothdc  3675  2if2dc  3680  ifeqeqxdc  3687  disjsn2  3772  diftpsn3  3856  elpr2elpr  3901  dfopg  3902  unimax  3969  sndisj  4126  eqbrtrrd  4154  breqtrrd  4158  breqtrrid  4168  eqbrtrrdi  4170  class2seteq  4300  opth1  4376  euotd  4395  opelopabsb  4402  tfisi  4734  0nelxp  4802  opeliunxp  4830  euiotaex  5354  iota4  5357  iotam  5369  fun2ssres  5421  funimass1  5458  funssfv  5721  fnimapr  5763  fvun1  5769  fvco4  5777  elfvmptrab  5802  fmptco  5874  fncofn  5893  foima2  5957  foeqcnvco  5996  f1eqcocnv  5997  f1oiso2  6033  riotass2  6067  riotass  6068  f1ocnvfv3  6074  fvmpopr2d  6225  caovlem2d  6282  f1opw2  6296  offveq  6323  sbcopeq1a  6421  csbopeq1a  6422  eloprabi  6432  cnvf1olem  6460  f2ndf  6462  suppval1  6479  suppsnopdc  6490  smoiso  6573  nnaword  6784  eqer  6839  uniqs  6867  mapsncnv  6977  ixpiinm  7006  mapsnf1o  7019  mapunen  7151  ssenen  7152  findcard2  7193  findcard2s  7194  unsnfidcex  7227  fisseneq  7242  phpeqd  7243  en1eqsn  7265  sbthlemi6  7279  updjud  7422  omp1eomlem  7434  nnnninf2  7467  nninfisollem0  7470  nninfisollemeq  7472  fodju0  7487  3nsssucpw1  7595  enq0sym  7799  enq0tr  7801  recexgt0sr  8140  caucvgsrlemoffcau  8165  axcaucvglemval  8264  le2tri3i  8435  cnegexlem2  8503  nnpcan  8550  addlsub  8697  negf1o  8710  subdi  8713  rereim  8916  cru  8932  divmulassap  9027  divmulasscomap  9028  divap1d  9133  subhalfhalf  9544  div4p1lem1div2  9563  difgtsumgt  9718  elz2  9720  zindd  9768  qapne  10048  divge1  10134  xrlttri3  10209  fseq1p1m1  10511  fzrevral  10522  nn0disj  10555  fzo0addel  10616  fzosplitsnm1  10637  fzosplitprm1  10663  flqlelt  10722  flaplelt  10723  divfl0  10744  flqpmodeq  10777  zmodidfzo  10803  modqmuladd  10816  qnegmod  10819  addmodid  10822  modifeq2int  10836  modqeqmodmin  10844  modfzo0difsn  10845  modsumfzodifsn  10846  addmodlteq  10848  frecuzrdgsuc  10864  frecfzen2  10877  iseqf1olemab  10952  iseqf1olemmo  10955  seqf1oglem1  10969  seqf1oglem2  10970  ser3sub  10973  expgt1  11027  leexp2r  11043  sqoddm1div8  11144  mulsubdivbinom2ap  11163  bcm1k  11212  bcn2m1  11222  hashinfuni  11230  hashennnuni  11232  hashennn  11233  hashunlem  11258  hashprg  11263  fihashssdif  11273  hashfibclem  11296  hashfibc  11297  hashf1lem1  11299  hashf1lem2  11300  zfz1isolem1  11306  elovmpowrd  11360  ccatsymb  11384  ccatlid  11388  eqs1  11410  ccatw2s1p1g  11427  swrdfv2  11449  swrds1  11454  swrdlsw  11455  pfxfv  11470  swrdswrd  11491  swrdpfx  11493  pfxpfx  11494  pfxlswccat  11499  ccats1pfxeq  11500  wrdind  11508  wrd2ind  11509  pfxccatin12lem1  11514  pfxccatin12lem2  11517  swrdccat3blem  11525  swrdccat3b  11526  ccats1pfxeqbi  11528  reuccatpfxs1lem  11532  reuccatpfxs1  11533  s3s4d  11589  s2s5d  11590  s5s2d  11591  shftlem  11595  shftfvalg  11597  shftfval  11600  replim  11638  cjexp  11672  sq01  11674  resqrexlemcalc1  11794  resqrexlemcvg  11799  rersqrtthlem  11810  abssq  11862  recan  11890  negfi  12009  minclpr  12018  mingeb  12024  xrmaxiflemcom  12031  xrmineqinf  12051  xrminltinf  12054  xrminadd  12057  climmpt  12082  climrecl  12106  fsum3cvg  12161  summodclem3  12163  summodclem2a  12164  modfsummodlemstep  12240  isumsplit  12274  arisum  12281  geosergap  12289  geo2sum  12297  mertenslemi1  12318  mertenslem2  12319  clim2divap  12323  fproddccvg  12355  fprodssdc  12373  fprodabs  12399  fproddivapf  12414  fprodmodd  12424  efcj  12456  efsub  12464  eflegeo  12484  sinneg  12509  cosneg  12510  sin01bnd  12540  cos01bnd  12541  modm1div  12583  summodnegmod  12605  dvdseq  12631  addmodlteqALT  12642  mulmoddvds  12646  zob  12674  nn0ob  12691  divalgmod  12710  flodddiv4  12719  bitsinv1  12745  divgcdnnr  12769  gcdneg  12775  bezoutlemsup  12802  dvdssq  12824  lcmneg  12868  3lcm2e6woprm  12880  6lcm4e12  12881  divgcdcoprmex  12896  cncongr1  12897  cncongrcoprm  12900  nnmaxpwlemxy  12964  nnmaxpwlemnfac  12967  divnumden  12992  zgcdsq  12997  phibnd  13015  hashgcdlem  13036  vfermltl  13050  powm2modprm  13051  reumodprminv  13052  pythagtriplem19  13081  pcprendvds2  13090  pczpre  13096  dvdsprmpweqle  13136  difsqpwdvds  13137  4sqlem4  13191  prmlem0  13240  ballotfilemfp1  13280  ballotfilemsf1o  13306  ballotfilemrinv0  13325  ennnfonelemex  13354  strndxid  13429  topnvalg  13654  intopsn  13736  ismgmid2  13749  mgmidsssn0  13753  gzsumfzval  13760  mndpfo  13800  mndfo  13801  mndinvmod  13807  mnd1id  13812  mhmf1o  13826  0mhm  13842  gzsumwmhm  13852  grpidd2  13895  grpinvid2  13907  grpidssd  13930  grpnpcan  13946  grpsubsub4  13947  qusgrp2  13965  mulginvcom  13999  grpissubg  14046  quselbasg  14082  qus0  14087  ecqusaddd  14090  ghmid  14101  ghminv  14102  imasabl  14189  gzsummhm  14194  gzsumsplit0  14197  gzsumshift  14198  gsumsncmn  14205  prdssca  14224  prds0g  14244  mgpress  14279  rnglz  14293  rngrz  14294  rngmneg1  14295  rngmneg2  14296  rngpropd  14303  rng1zrlem  14307  srgmulgass  14342  srgpcomp  14343  srgpcomppsc  14345  ringadd2  14381  ringo2times  14382  ringlz  14397  ringrz  14398  ringinvnzdiv  14404  ringnegl  14405  ringnegr  14406  imasring  14418  qusring2  14420  crngunit  14467  rhmopp  14532  lringuplu  14552  opprdomnbg  14632  lmod0vs  14707  lmodvsmmulgdi  14709  lmodfopne  14712  islss3  14765  lspsn  14802  lmodindp1  14814  rnglidlmmgm  14882  rnglidlmsgrp  14883  rnglidlrng  14884  isridl  14890  zringinvg  14988  zndvds  15033  znf1o  15035  assa2ass  15058  assa2ass2  15059  asclinvg  15081  assamulgscmlem1  15090  assamulgscmlem2  15091  psrgrp  15125  toponcom  15177  tgtopon  15216  restopnb  15331  cnptoprest  15389  blfvalps  15535  bdmopn  15654  cnmet  15680  mpomulcn  15716  limcdifap  15812  dvidsslem  15843  dviaddf  15855  dvexp  15861  dvply2g  15916  coseq0negpitopi  15987  abssinper  15997  rplogbzexp  16109  pellexlem2  16149  dvdsppwf1o  16184  mpodvdsmulf1o  16185  fsumdvdsmul  16186  sgmmul  16191  perfect  16199  bcmono  16202  prmefexple  16206  bposlem1  16209  lgsvalmod  16236  lgsneg  16241  gausslemma2dlem1a  16275  gausslemma2dlem6  16284  gausslemma2dlem7  16285  gausslemma2d  16286  lgsquadlem2  16295  2lgslem1a1  16303  2lgslem1a  16305  2lgslem3c  16312  2lgslem3d  16313  2lgslem3d1  16317  2lgs  16321  2lgsoddprm  16330  uhgrun  16425  upgrun  16465  umgrun  16467  ushgredgedg  16565  issubgr2  16597  uhgrissubgr  16600  subgruhgredgdm  16609  subumgredg2en  16610  subupgr  16612  p1evtxdeqfilem  16650  wlklenvm1  16680  wlklenvm1g  16681  wlkl1loop  16697  upgriswlkdc  16699  uspgr2wlkeq  16704  uspgr2wlkeq2  16705  uspgr2wlkeqi  16706  wlkres  16718  loopclwwlkn1b  16758  clwwlkn1loopb  16759  clwwlkext2edg  16761  clwwlknonccat  16772  s2elclwwlknon2  16775  clwwlknonex2lem2  16777  clwwlknun  16780  eupth2lem3fi  16815  eupth2lembfi  16816  subctctexmid  17128  cvgcmp2nlemabs  17179  trilpolemlt1  17188