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  4155  breqtrrd  4159  breqtrrid  4169  eqbrtrrdi  4171  class2seteq  4302  opth1  4378  euotd  4397  opelopabsb  4404  tfisi  4736  0nelxp  4804  opeliunxp  4832  euiotaex  5357  iota4  5360  iotam  5372  fun2ssres  5424  funimass1  5461  funssfv  5724  fnimapr  5766  fvun1  5772  fvco4  5780  elfvmptrab  5805  fmptco  5877  fncofn  5896  foima2  5960  foeqcnvco  5999  f1eqcocnv  6000  f1oiso2  6036  riotass2  6070  riotass  6071  f1ocnvfv3  6077  fvmpopr2d  6228  caovlem2d  6285  f1opw2  6299  offveq  6327  sbcopeq1a  6425  csbopeq1a  6426  eloprabi  6436  cnvf1olem  6464  f2ndf  6466  suppval1  6483  suppsnopdc  6494  smoiso  6577  nnaword  6788  eqer  6843  uniqs  6871  mapsncnv  6981  ixpiinm  7010  mapsnf1o  7023  mapunen  7155  ssenen  7156  findcard2  7197  findcard2s  7198  unsnfidcex  7231  fisseneq  7246  phpeqd  7247  en1eqsn  7270  sbthlemi6  7284  updjud  7428  omp1eomlem  7440  nnnninf2  7473  nninfisollem0  7476  nninfisollemeq  7478  fodju0  7493  3nsssucpw1  7601  enq0sym  7805  enq0tr  7807  recexgt0sr  8146  caucvgsrlemoffcau  8171  axcaucvglemval  8270  le2tri3i  8441  cnegexlem2  8509  nnpcan  8556  addlsub  8703  negf1o  8716  subdi  8719  rereim  8922  cru  8938  divmulassap  9033  divmulasscomap  9034  divap1d  9139  subhalfhalf  9551  div4p1lem1div2  9570  difgtsumgt  9725  elz2  9727  zindd  9775  qapne  10055  divge1  10141  xrlttri3  10216  fseq1p1m1  10518  fzrevral  10529  nn0disj  10562  fzo0addel  10623  fzosplitsnm1  10644  fzosplitprm1  10670  flqlelt  10729  flaplelt  10730  divfl0  10752  flqpmodeq  10785  zmodidfzo  10811  modqmuladd  10824  qnegmod  10827  addmodid  10830  modifeq2int  10844  modqeqmodmin  10852  modfzo0difsn  10853  modsumfzodifsn  10854  addmodlteq  10856  frecuzrdgsuc  10872  frecfzen2  10885  iseqf1olemab  10960  iseqf1olemmo  10963  seqf1oglem1  10977  seqf1oglem2  10978  ser3sub  10981  expgt1  11035  leexp2r  11051  sqoddm1div8  11152  mulsubdivbinom2ap  11171  bcm1k  11220  bcn2m1  11230  hashinfuni  11238  hashennnuni  11240  hashennn  11241  hashunlem  11266  hashprg  11271  fihashssdif  11281  hashfibclem  11304  hashfibc  11305  hashf1lem1  11307  hashf1lem2  11308  zfz1isolem1  11314  elovmpowrd  11368  ccatsymb  11392  ccatlid  11396  eqs1  11418  ccatw2s1p1g  11435  swrdfv2  11457  swrds1  11462  swrdlsw  11463  pfxfv  11478  swrdswrd  11499  swrdpfx  11501  pfxpfx  11502  pfxlswccat  11507  ccats1pfxeq  11508  wrdind  11516  wrd2ind  11517  pfxccatin12lem1  11522  pfxccatin12lem2  11525  swrdccat3blem  11533  swrdccat3b  11534  ccats1pfxeqbi  11536  reuccatpfxs1lem  11540  reuccatpfxs1  11541  s3s4d  11597  s2s5d  11598  s5s2d  11599  shftlem  11603  shftfvalg  11605  shftfval  11608  replim  11646  cjexp  11680  sq01  11682  resqrexlemcalc1  11802  resqrexlemcvg  11807  rersqrtthlem  11818  abssq  11870  recan  11898  negfi  12017  minclpr  12027  mingeb  12033  xrmaxiflemcom  12040  xrmineqinf  12060  xrminltinf  12063  xrminadd  12066  climmpt  12091  climrecl  12115  fsum3cvg  12170  summodclem3  12172  summodclem2a  12173  modfsummodlemstep  12249  isumsplit  12283  arisum  12290  geosergap  12298  geo2sum  12306  mertenslemi1  12327  mertenslem2  12328  clim2divap  12332  fproddccvg  12364  fprodssdc  12382  fprodabs  12408  fproddivapf  12423  fprodmodd  12433  efcj  12465  efsub  12473  eflegeo  12493  sinneg  12518  cosneg  12519  sin01bnd  12549  cos01bnd  12550  modm1div  12592  summodnegmod  12614  dvdseq  12640  addmodlteqALT  12651  mulmoddvds  12655  zob  12683  nn0ob  12700  divalgmod  12719  flodddiv4  12728  bitsinv1  12754  divgcdnnr  12778  gcdneg  12784  bezoutlemsup  12811  dvdssq  12833  lcmneg  12877  3lcm2e6woprm  12889  6lcm4e12  12890  divgcdcoprmex  12905  cncongr1  12906  cncongrcoprm  12909  nnmaxpwlemxy  12973  nnmaxpwlemnfac  12976  divnumden  13001  zgcdsq  13006  phibnd  13024  hashgcdlem  13045  vfermltl  13059  powm2modprm  13060  reumodprminv  13061  pythagtriplem19  13090  pcprendvds2  13099  pczpre  13105  dvdsprmpweqle  13145  difsqpwdvds  13146  4sqlem4  13200  prmlem0  13249  ballotfilemfp1  13289  ballotfilemsf1o  13315  ballotfilemrinv0  13334  ennnfonelemex  13363  strndxid  13438  topnvalg  13664  intopsn  13746  ismgmid2  13759  mgmidsssn0  13763  gzsumfzval  13770  mndpfo  13810  mndfo  13811  mndinvmod  13817  mnd1id  13822  mhmf1o  13836  0mhm  13852  gzsumwmhm  13862  grpidd2  13905  grpinvid2  13917  grpidssd  13940  grpnpcan  13956  grpsubsub4  13957  qusgrp2  13975  mulginvcom  14009  grpissubg  14056  quselbasg  14092  qus0  14097  ecqusaddd  14100  ghmid  14111  ghminv  14112  cntrval  14151  imasabl  14230  gzsummhm  14235  gzsumsplit0  14238  gzsumshift  14239  gsumsncmn  14246  gsumcom2fi  14275  prdssca  14282  prds0g  14302  mgpress  14337  rnglz  14351  rngrz  14352  rngmneg1  14353  rngmneg2  14354  rngpropd  14361  rng1zrlem  14365  srgmulgass  14400  srgpcomp  14401  srgpcomppsc  14403  ringadd2  14439  ringo2times  14440  ringlz  14455  ringrz  14456  ringinvnzdiv  14462  ringnegl  14463  ringnegr  14464  imasring  14478  qusring2  14480  crngunit  14527  rhmopp  14592  lringuplu  14612  opprdomnbg  14692  lmod0vs  14767  lmodvsmmulgdi  14769  lmodfopne  14772  islss3  14825  lspsn  14862  lmodindp1  14874  rnglidlmmgm  14942  rnglidlmsgrp  14943  rnglidlrng  14944  isridl  14950  zringinvg  15048  zndvds  15093  znf1o  15095  assa2ass  15118  assa2ass2  15119  asclinvg  15141  assamulgscmlem1  15150  assamulgscmlem2  15151  psrgrp  15195  toponcom  15253  tgtopon  15292  restopnb  15407  cnptoprest  15465  blfvalps  15611  bdmopn  15730  cnmet  15756  mpomulcn  15792  limcdifap  15888  dvidsslem  15919  dviaddf  15931  dvexp  15937  dvply2g  15992  coseq0negpitopi  16063  abssinper  16073  rplogbzexp  16190  pellexlem2  16230  dvdsppwf1o  16283  mpodvdsmulf1o  16284  fsumdvdsmul  16285  sgmmul  16290  perfect  16301  bcmono  16304  prmefexple  16308  bposlem1  16311  bposlem9  16319  lgsvalmod  16343  lgsneg  16348  gausslemma2dlem1a  16382  gausslemma2dlem6  16391  gausslemma2dlem7  16392  gausslemma2d  16393  lgsquadlem2  16402  2lgslem1a1  16410  2lgslem1a  16412  2lgslem3c  16419  2lgslem3d  16420  2lgslem3d1  16424  2lgs  16428  2lgsoddprm  16437  uhgrun  16532  upgrun  16572  umgrun  16574  ushgredgedg  16672  issubgr2  16704  uhgrissubgr  16707  subgruhgredgdm  16716  subumgredg2en  16717  subupgr  16719  p1evtxdeqfilem  16757  wlklenvm1  16787  wlklenvm1g  16788  wlkl1loop  16804  upgriswlkdc  16806  uspgr2wlkeq  16811  uspgr2wlkeq2  16812  uspgr2wlkeqi  16813  wlkres  16825  loopclwwlkn1b  16865  clwwlkn1loopb  16866  clwwlkext2edg  16868  clwwlknonccat  16879  s2elclwwlknon2  16882  clwwlknonex2lem2  16884  clwwlknun  16887  eupth2lem3fi  16922  eupth2lembfi  16923  subctctexmid  17235  cvgcmp2nlemabs  17287  trilpolemlt1  17297