Theorem eqcomd 2235

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-ext 2211

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

This theorem is referenced by:  eqtr2d  2263  eqtr3d  2264  eqtr4d  2265  eqtr2id  2275  eqtr2di  2279  sylan9req  2283  eqeltrrd  2307  eleqtrrd  2309  eleqtrrid  2319  eqeltrrdi  2321  eqnetrrd  2426  neeqtrrd  2430  rspcedeq2vd  2917  dedhb  2972  eqsstrrd  3261  sseqtrrd  3263  eqsstrrdi  3277  dfrab3ss  3482  uneqdifeqim  3577  ifbothdadc  3636  ifbothdc  3637  2if2dc  3642  disjsn2  3729  diftpsn3  3808  elpr2elpr  3853  dfopg  3854  unimax  3921  sndisj  4078  eqbrtrrd  4106  breqtrrd  4110  breqtrrid  4120  eqbrtrrdi  4122  class2seteq  4246  opth1  4321  euotd  4340  opelopabsb  4347  tfisi  4678  0nelxp  4746  opeliunxp  4773  euiotaex  5294  iota4  5297  iotam  5309  fun2ssres  5360  funimass1  5397  funssfv  5652  fnimapr  5693  fvun1  5699  fvco4  5705  elfvmptrab  5729  fmptco  5800  foima2  5874  foeqcnvco  5913  f1eqcocnv  5914  f1oiso2  5950  riotass2  5982  riotass  5983  f1ocnvfv3  5989  fvmpopr2d  6140  caovlem2d  6197  f1opw2  6210  offveq  6237  sbcopeq1a  6331  csbopeq1a  6332  eloprabi  6340  cnvf1olem  6368  f2ndf  6370  smoiso  6446  nnaword  6655  eqer  6710  uniqs  6738  mapsncnv  6840  ixpiinm  6869  mapsnf1o  6882  ssenen  7008  findcard2  7047  findcard2s  7048  unsnfidcex  7078  fisseneq  7092  phpeqd  7093  en1eqsn  7111  sbthlemi6  7125  updjud  7245  omp1eomlem  7257  nnnninf2  7290  nninfisollem0  7293  nninfisollemeq  7295  fodju0  7310  3nsssucpw1  7417  enq0sym  7615  enq0tr  7617  recexgt0sr  7956  caucvgsrlemoffcau  7981  axcaucvglemval  8080  le2tri3i  8251  cnegexlem2  8318  nnpcan  8365  addlsub  8512  negf1o  8524  subdi  8527  rereim  8729  cru  8745  divmulassap  8838  divmulasscomap  8839  divap1d  8944  subhalfhalf  9342  div4p1lem1div2  9361  difgtsumgt  9512  elz2  9514  zindd  9561  qapne  9830  divge1  9915  xrlttri3  9989  fseq1p1m1  10286  fzrevral  10297  nn0disj  10330  fzo0addel  10389  fzosplitsnm1  10410  fzosplitprm1  10435  flqlelt  10491  divfl0  10511  flqpmodeq  10544  zmodidfzo  10570  modqmuladd  10583  qnegmod  10586  addmodid  10589  modifeq2int  10603  modqeqmodmin  10611  modfzo0difsn  10612  modsumfzodifsn  10613  addmodlteq  10615  frecuzrdgsuc  10631  frecfzen2  10644  iseqf1olemab  10719  iseqf1olemmo  10722  seqf1oglem1  10736  seqf1oglem2  10737  ser3sub  10740  expgt1  10794  leexp2r  10810  sqoddm1div8  10910  mulsubdivbinom2ap  10928  bcm1k  10977  bcn2m1  10986  hashinfuni  10994  hashennnuni  10996  hashennn  10997  hashunlem  11021  hashprg  11025  fihashssdif  11035  zfz1isolem1  11057  elovmpowrd  11108  ccatsymb  11132  ccatlid  11136  eqs1  11156  swrdfv2  11190  swrds1  11195  swrdlsw  11196  pfxfv  11211  swrdswrd  11232  swrdpfx  11234  pfxpfx  11235  pfxlswccat  11240  ccats1pfxeq  11241  wrdind  11249  wrd2ind  11250  pfxccatin12lem1  11255  pfxccatin12lem2  11258  swrdccat3blem  11266  swrdccat3b  11267  ccats1pfxeqbi  11269  reuccatpfxs1lem  11273  reuccatpfxs1  11274  shftlem  11322  shftfvalg  11324  shftfval  11327  replim  11365  cjexp  11399  resqrexlemcalc1  11520  resqrexlemcvg  11525  rersqrtthlem  11536  abssq  11587  recan  11615  negfi  11734  minclpr  11743  mingeb  11748  xrmaxiflemcom  11755  xrmineqinf  11775  xrminltinf  11778  xrminadd  11781  climmpt  11806  climrecl  11830  fsum3cvg  11884  summodclem3  11886  summodclem2a  11887  modfsummodlemstep  11963  isumsplit  11997  arisum  12004  geosergap  12012  geo2sum  12020  mertenslemi1  12041  mertenslem2  12042  clim2divap  12046  fproddccvg  12078  fprodssdc  12096  fprodabs  12122  fproddivapf  12137  fprodmodd  12147  efcj  12179  efsub  12187  eflegeo  12207  sinneg  12232  cosneg  12233  sin01bnd  12263  cos01bnd  12264  modm1div  12306  summodnegmod  12328  dvdseq  12354  addmodlteqALT  12365  mulmoddvds  12369  zob  12397  nn0ob  12414  divalgmod  12433  flodddiv4  12442  bitsinv1  12468  divgcdnnr  12492  gcdneg  12498  bezoutlemsup  12525  dvdssq  12547  lcmneg  12591  3lcm2e6woprm  12603  6lcm4e12  12604  divgcdcoprmex  12619  cncongr1  12620  cncongrcoprm  12623  oddpwdclemxy  12686  oddpwdclemodd  12689  divnumden  12713  zgcdsq  12718  phibnd  12734  hashgcdlem  12755  vfermltl  12769  powm2modprm  12770  reumodprminv  12771  pythagtriplem19  12800  pcprendvds2  12809  pczpre  12815  dvdsprmpweqle  12855  difsqpwdvds  12856  4sqlem4  12910  ennnfonelemex  12980  strndxid  13055  topnvalg  13279  prdssca  13303  intopsn  13395  ismgmid2  13408  mgmidsssn0  13412  gsumfzval  13419  gsumprval  13427  mndpfo  13466  mndfo  13467  mndinvmod  13473  prds0g  13477  mnd1id  13484  mhmf1o  13498  0mhm  13514  gsumwmhm  13526  grpidd2  13569  grpinvid2  13581  grpidssd  13604  grpnpcan  13620  grpsubsub4  13621  qusgrp2  13645  mulginvcom  13679  grpissubg  13726  quselbasg  13762  qus0  13767  ecqusaddd  13770  ghmid  13781  ghminv  13782  imasabl  13868  gsumfzmhm  13875  mgpress  13889  rnglz  13903  rngrz  13904  rngmneg1  13905  rngmneg2  13906  rngpropd  13913  srg1zr  13945  srgmulgass  13947  srgpcomp  13948  srgpcomppsc  13950  ringadd2  13985  ringo2times  13986  ringlz  14001  ringrz  14002  ringinvnzdiv  14008  ringnegl  14009  ringnegr  14010  imasring  14022  qusring2  14024  crngunit  14069  rhmopp  14134  lringuplu  14154  opprdomnbg  14232  lmod0vs  14279  lmodvsmmulgdi  14281  lmodfopne  14284  islss3  14337  lspsn  14374  lmodindp1  14386  rnglidlmmgm  14454  rnglidlmsgrp  14455  rnglidlrng  14456  isridl  14462  zringinvg  14562  zndvds  14607  znf1o  14609  psrgrp  14643  toponcom  14695  tgtopon  14734  restopnb  14849  cnptoprest  14907  blfvalps  15053  bdmopn  15172  cnmet  15198  mpomulcn  15234  limcdifap  15330  dvidsslem  15361  dviaddf  15373  dvexp  15379  dvply2g  15434  coseq0negpitopi  15504  abssinper  15514  rplogbzexp  15622  dvdsppwf1o  15657  mpodvdsmulf1o  15658  fsumdvdsmul  15659  sgmmul  15664  perfect  15669  lgsvalmod  15692  lgsneg  15697  gausslemma2dlem1a  15731  gausslemma2dlem6  15740  gausslemma2dlem7  15741  gausslemma2d  15742  lgsquadlem2  15751  2lgslem1a1  15759  2lgslem1a  15761  2lgslem3c  15768  2lgslem3d  15769  2lgslem3d1  15773  2lgs  15777  2lgsoddprm  15786  uhgrun  15880  upgrun  15918  umgrun  15920  ushgredgedg  16018  wlklenvm1g  16039  subctctexmid  16325  cvgcmp2nlemabs  16359  trilpolemlt1  16368