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  8434  cnegexlem2  8502  nnpcan  8549  addlsub  8696  negf1o  8709  subdi  8712  rereim  8914  cru  8930  divmulassap  9025  divmulasscomap  9026  divap1d  9131  subhalfhalf  9540  div4p1lem1div2  9559  difgtsumgt  9714  elz2  9716  zindd  9764  qapne  10039  divge1  10124  xrlttri3  10199  fseq1p1m1  10501  fzrevral  10512  nn0disj  10545  fzo0addel  10606  fzosplitsnm1  10627  fzosplitprm1  10653  flqlelt  10711  divfl0  10731  flqpmodeq  10764  zmodidfzo  10790  modqmuladd  10803  qnegmod  10806  addmodid  10809  modifeq2int  10823  modqeqmodmin  10831  modfzo0difsn  10832  modsumfzodifsn  10833  addmodlteq  10835  frecuzrdgsuc  10851  frecfzen2  10864  iseqf1olemab  10939  iseqf1olemmo  10942  seqf1oglem1  10956  seqf1oglem2  10957  ser3sub  10960  expgt1  11014  leexp2r  11030  sqoddm1div8  11131  mulsubdivbinom2ap  11149  bcm1k  11198  bcn2m1  11208  hashinfuni  11216  hashennnuni  11218  hashennn  11219  hashunlem  11244  hashprg  11249  fihashssdif  11259  hashfibclem  11282  hashfibc  11283  hashf1lem1  11285  hashf1lem2  11286  zfz1isolem1  11292  elovmpowrd  11346  ccatsymb  11370  ccatlid  11374  eqs1  11396  ccatw2s1p1g  11413  swrdfv2  11435  swrds1  11440  swrdlsw  11441  pfxfv  11456  swrdswrd  11477  swrdpfx  11479  pfxpfx  11480  pfxlswccat  11485  ccats1pfxeq  11486  wrdind  11494  wrd2ind  11495  pfxccatin12lem1  11500  pfxccatin12lem2  11503  swrdccat3blem  11511  swrdccat3b  11512  ccats1pfxeqbi  11514  reuccatpfxs1lem  11518  reuccatpfxs1  11519  s3s4d  11575  s2s5d  11576  s5s2d  11577  shftlem  11581  shftfvalg  11583  shftfval  11586  replim  11624  cjexp  11658  sq01  11660  resqrexlemcalc1  11780  resqrexlemcvg  11785  rersqrtthlem  11796  abssq  11847  recan  11875  negfi  11994  minclpr  12003  mingeb  12008  xrmaxiflemcom  12015  xrmineqinf  12035  xrminltinf  12038  xrminadd  12041  climmpt  12066  climrecl  12090  fsum3cvg  12145  summodclem3  12147  summodclem2a  12148  modfsummodlemstep  12224  isumsplit  12258  arisum  12265  geosergap  12273  geo2sum  12281  mertenslemi1  12302  mertenslem2  12303  clim2divap  12307  fproddccvg  12339  fprodssdc  12357  fprodabs  12383  fproddivapf  12398  fprodmodd  12408  efcj  12440  efsub  12448  eflegeo  12468  sinneg  12493  cosneg  12494  sin01bnd  12524  cos01bnd  12525  modm1div  12567  summodnegmod  12589  dvdseq  12615  addmodlteqALT  12626  mulmoddvds  12630  zob  12658  nn0ob  12675  divalgmod  12694  flodddiv4  12703  bitsinv1  12729  divgcdnnr  12753  gcdneg  12759  bezoutlemsup  12786  dvdssq  12808  lcmneg  12852  3lcm2e6woprm  12864  6lcm4e12  12865  divgcdcoprmex  12880  cncongr1  12881  cncongrcoprm  12884  oddpwdclemxy  12947  oddpwdclemodd  12950  divnumden  12974  zgcdsq  12979  phibnd  12995  hashgcdlem  13016  vfermltl  13030  powm2modprm  13031  reumodprminv  13032  pythagtriplem19  13061  pcprendvds2  13070  pczpre  13076  dvdsprmpweqle  13116  difsqpwdvds  13117  4sqlem4  13171  ballotfilemfp1  13231  ballotfilemsf1o  13257  ballotfilemrinv0  13276  ennnfonelemex  13305  strndxid  13380  topnvalg  13605  intopsn  13687  ismgmid2  13700  mgmidsssn0  13704  gzsumfzval  13711  mndpfo  13751  mndfo  13752  mndinvmod  13758  mnd1id  13763  mhmf1o  13777  0mhm  13793  gzsumwmhm  13803  grpidd2  13846  grpinvid2  13858  grpidssd  13881  grpnpcan  13897  grpsubsub4  13898  qusgrp2  13916  mulginvcom  13950  grpissubg  13997  quselbasg  14033  qus0  14038  ecqusaddd  14041  ghmid  14052  ghminv  14053  imasabl  14140  gzsummhm  14145  gzsumsplit0  14148  gzsumshift  14149  gsumsncmn  14156  prdssca  14175  prds0g  14195  mgpress  14230  rnglz  14244  rngrz  14245  rngmneg1  14246  rngmneg2  14247  rngpropd  14254  rng1zrlem  14258  srgmulgass  14293  srgpcomp  14294  srgpcomppsc  14296  ringadd2  14332  ringo2times  14333  ringlz  14348  ringrz  14349  ringinvnzdiv  14355  ringnegl  14356  ringnegr  14357  imasring  14369  qusring2  14371  crngunit  14418  rhmopp  14483  lringuplu  14503  opprdomnbg  14583  lmod0vs  14658  lmodvsmmulgdi  14660  lmodfopne  14663  islss3  14716  lspsn  14753  lmodindp1  14765  rnglidlmmgm  14833  rnglidlmsgrp  14834  rnglidlrng  14835  isridl  14841  zringinvg  14939  zndvds  14984  znf1o  14986  assa2ass  15009  assa2ass2  15010  asclinvg  15032  assamulgscmlem1  15041  assamulgscmlem2  15042  psrgrp  15076  toponcom  15128  tgtopon  15167  restopnb  15282  cnptoprest  15340  blfvalps  15486  bdmopn  15605  cnmet  15631  mpomulcn  15667  limcdifap  15763  dvidsslem  15794  dviaddf  15806  dvexp  15812  dvply2g  15867  coseq0negpitopi  15937  abssinper  15947  rplogbzexp  16056  pellexlem2  16092  dvdsppwf1o  16103  mpodvdsmulf1o  16104  fsumdvdsmul  16105  sgmmul  16110  perfect  16115  lgsvalmod  16138  lgsneg  16143  gausslemma2dlem1a  16177  gausslemma2dlem6  16186  gausslemma2dlem7  16187  gausslemma2d  16188  lgsquadlem2  16197  2lgslem1a1  16205  2lgslem1a  16207  2lgslem3c  16214  2lgslem3d  16215  2lgslem3d1  16219  2lgs  16223  2lgsoddprm  16232  uhgrun  16327  upgrun  16367  umgrun  16369  ushgredgedg  16467  issubgr2  16499  uhgrissubgr  16502  subgruhgredgdm  16511  subumgredg2en  16512  subupgr  16514  p1evtxdeqfilem  16552  wlklenvm1  16582  wlklenvm1g  16583  wlkl1loop  16599  upgriswlkdc  16601  uspgr2wlkeq  16606  uspgr2wlkeq2  16607  uspgr2wlkeqi  16608  wlkres  16620  loopclwwlkn1b  16660  clwwlkn1loopb  16661  clwwlkext2edg  16663  clwwlknonccat  16674  s2elclwwlknon2  16677  clwwlknonex2lem2  16679  clwwlknun  16682  eupth2lem3fi  16717  eupth2lembfi  16718  subctctexmid  17030  cvgcmp2nlemabs  17081  trilpolemlt1  17090