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  6578  nnaword  6789  eqer  6844  uniqs  6872  mapsncnv  6983  ixpiinm  7012  mapsnf1o  7025  mapunen  7157  ssenen  7158  findcard2  7199  findcard2s  7200  unsnfidcex  7233  fisseneq  7248  phpeqd  7249  en1eqsn  7272  sbthlemi6  7286  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  9723  elz2  9725  zindd  9774  qapne  10054  divge1  10140  xrlttri3  10215  fseq1p1m1  10517  fzrevral  10528  nn0disj  10561  fzo0addel  10622  fzosplitsnm1  10643  fzosplitprm1  10669  flqlelt  10728  flaplelt  10729  divfl0  10751  flqpmodeq  10784  zmodidfzo  10810  modqmuladd  10823  qnegmod  10826  addmodid  10829  modifeq2int  10843  modqeqmodmin  10851  modfzo0difsn  10852  modsumfzodifsn  10853  addmodlteq  10855  frecuzrdgsuc  10871  frecfzen2  10884  iseqf1olemab  10959  iseqf1olemmo  10962  seqf1oglem1  10976  seqf1oglem2  10977  ser3sub  10980  expgt1  11034  leexp2r  11050  sqoddm1div8  11151  mulsubdivbinom2ap  11170  bcm1k  11219  bcn2m1  11229  hashinfuni  11237  hashennnuni  11239  hashennn  11240  hashunlem  11265  hashprg  11270  fihashssdif  11280  hashfibclem  11303  hashfibc  11304  hashf1lem1  11306  hashf1lem2  11307  zfz1isolem1  11313  elovmpowrd  11367  ccatsymb  11391  ccatlid  11395  eqs1  11417  ccatw2s1p1g  11434  swrdfv2  11456  swrds1  11461  swrdlsw  11462  pfxfv  11477  swrdswrd  11498  swrdpfx  11500  pfxpfx  11501  pfxlswccat  11506  ccats1pfxeq  11507  wrdind  11515  wrd2ind  11516  pfxccatin12lem1  11521  pfxccatin12lem2  11524  swrdccat3blem  11532  swrdccat3b  11533  ccats1pfxeqbi  11535  reuccatpfxs1lem  11539  reuccatpfxs1  11540  s3s4d  11596  s2s5d  11597  s5s2d  11598  shftlem  11602  shftfvalg  11604  shftfval  11607  replim  11645  cjexp  11679  sq01  11681  resqrexlemcalc1  11801  resqrexlemcvg  11806  rersqrtthlem  11817  abssq  11869  recan  11897  negfi  12016  minclpr  12026  mingeb  12032  xrmaxiflemcom  12039  xrmineqinf  12059  xrminltinf  12062  xrminadd  12065  climmpt  12090  climrecl  12114  fsum3cvg  12169  summodclem3  12171  summodclem2a  12172  modfsummodlemstep  12248  isumsplit  12282  arisum  12289  geosergap  12297  geo2sum  12305  mertenslemi1  12326  mertenslem2  12327  clim2divap  12331  fproddccvg  12363  fprodssdc  12381  fprodabs  12407  fproddivapf  12422  fprodmodd  12432  efcj  12464  efsub  12472  eflegeo  12492  sinneg  12517  cosneg  12518  sin01bnd  12548  cos01bnd  12549  modm1div  12591  summodnegmod  12613  dvdseq  12639  addmodlteqALT  12650  mulmoddvds  12654  zob  12682  nn0ob  12699  divalgmod  12718  flodddiv4  12727  bitsinv1  12753  divgcdnnr  12777  gcdneg  12783  bezoutlemsup  12810  dvdssq  12832  lcmneg  12876  3lcm2e6woprm  12888  6lcm4e12  12889  divgcdcoprmex  12904  cncongr1  12905  cncongrcoprm  12908  nnmaxpwlemxy  12972  nnmaxpwlemnfac  12975  divnumden  13000  zgcdsq  13005  phibnd  13023  hashgcdlem  13044  vfermltl  13058  powm2modprm  13059  reumodprminv  13060  pythagtriplem19  13089  pcprendvds2  13098  pczpre  13104  dvdsprmpweqle  13144  difsqpwdvds  13145  4sqlem4  13199  prmlem0  13248  ballotfilemfp1  13288  ballotfilemsf1o  13314  ballotfilemrinv0  13333  ennnfonelemex  13362  strndxid  13437  topnvalg  13663  intopsn  13745  ismgmid2  13758  mgmidsssn0  13762  gzsumfzval  13769  mndpfo  13809  mndfo  13810  mndinvmod  13816  mnd1id  13821  mhmf1o  13835  0mhm  13851  gzsumwmhm  13861  grpidd2  13904  grpinvid2  13916  grpidssd  13939  grpnpcan  13955  grpsubsub4  13956  qusgrp2  13974  mulginvcom  14008  grpissubg  14055  quselbasg  14091  qus0  14096  ecqusaddd  14099  ghmid  14110  ghminv  14111  cntrval  14150  imasabl  14229  gzsummhm  14234  gzsumsplit0  14237  gzsumshift  14238  gsumsncmn  14245  gsumcom2fi  14274  prdssca  14281  prds0g  14301  mgpress  14336  rnglz  14350  rngrz  14351  rngmneg1  14352  rngmneg2  14353  rngpropd  14360  rng1zrlem  14364  srgmulgass  14399  srgpcomp  14400  srgpcomppsc  14402  ringadd2  14438  ringo2times  14439  ringlz  14454  ringrz  14455  ringinvnzdiv  14461  ringnegl  14462  ringnegr  14463  imasring  14477  qusring2  14479  crngunit  14526  rhmopp  14591  lringuplu  14611  opprdomnbg  14691  lmod0vs  14766  lmodvsmmulgdi  14768  lmodfopne  14771  islss3  14824  lspsn  14861  lmodindp1  14873  rnglidlmmgm  14941  rnglidlmsgrp  14942  rnglidlrng  14943  isridl  14949  zringinvg  15047  zndvds  15092  znf1o  15094  assa2ass  15117  assa2ass2  15118  asclinvg  15140  assamulgscmlem1  15149  assamulgscmlem2  15150  psrgrp  15204  toponcom  15270  tgtopon  15309  restopnb  15424  cnptoprest  15482  blfvalps  15628  bdmopn  15747  cnmet  15773  mpomulcn  15809  limcdifap  15905  dvidsslem  15936  dviaddf  15948  dvexp  15954  dvply2g  16009  coseq0negpitopi  16080  abssinper  16090  rplogbzexp  16207  pellexlem2  16247  dvdsppwf1o  16300  mpodvdsmulf1o  16301  fsumdvdsmul  16302  sgmmul  16307  perfect  16318  bcmono  16321  prmefexple  16325  bposlem1  16328  bposlem9  16336  lgsvalmod  16360  lgsneg  16365  gausslemma2dlem1a  16399  gausslemma2dlem6  16408  gausslemma2dlem7  16409  gausslemma2d  16410  lgsquadlem2  16419  2lgslem1a1  16427  2lgslem1a  16429  2lgslem3c  16436  2lgslem3d  16437  2lgslem3d1  16441  2lgs  16445  2lgsoddprm  16454  uhgrun  16549  upgrun  16589  umgrun  16591  ushgredgedg  16689  issubgr2  16721  uhgrissubgr  16724  subgruhgredgdm  16733  subumgredg2en  16734  subupgr  16736  p1evtxdeqfilem  16774  wlklenvm1  16804  wlklenvm1g  16805  wlkl1loop  16821  upgriswlkdc  16823  uspgr2wlkeq  16828  uspgr2wlkeq2  16829  uspgr2wlkeqi  16830  wlkres  16842  loopclwwlkn1b  16882  clwwlkn1loopb  16883  clwwlkext2edg  16885  clwwlknonccat  16896  s2elclwwlknon2  16899  clwwlknonex2lem2  16901  clwwlknun  16904  eupth2lem3fi  16939  eupth2lembfi  16940  subctctexmid  17252  cvgcmp2nlemabs  17304  trilpolemlt1  17314