MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqcomd Unicode version

Theorem eqcomd 2288
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
StepHypRef Expression
1 eqcomd.1 . 2  |-  ( ph  ->  A  =  B )
2 eqcom 2285 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2sylib 188 1  |-  ( ph  ->  B  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  eqtr2d  2316  eqtr3d  2317  eqtr4d  2318  syl5req  2328  syl6req  2332  sylan9req  2336  eqeltrrd  2358  eleqtrrd  2360  syl5eleqr  2370  syl6eqelr  2372  eqnetrrd  2466  neeqtrrd  2470  dedhb  2935  eqsstr3d  3213  sseqtr4d  3215  syl6eqssr  3229  dfrab3ss  3446  uneqdifeq  3542  ifbi  3582  ifbothda  3595  dedth  3606  elimhyp  3613  elimhyp2v  3614  elimhyp3v  3615  elimhyp4v  3616  elimdhyp  3618  keephyp2v  3620  keephyp3v  3621  disjsn2  3694  unimax  3861  iununi  3986  sndisj  4015  disjprg  4019  eqbrtrrd  4045  breqtrrd  4049  syl5breqr  4059  syl6eqbrr  4061  class2seteq  4179  opth1  4244  euotd  4267  opelopabsb  4275  ordsuc  4605  tfisi  4649  0nelxp  4717  opeliunxp  4740  sosn  4759  somincom  5080  iotaex  5236  iota4  5237  fun2ssres  5295  funimass1  5325  funssfv  5543  fnimapr  5583  fvun  5589  fmptco  5691  foeqcnvco  5804  f1eqcocnv  5805  f1oiso2  5849  f1opw2  6071  sbcopeq1a  6172  csbopeq1a  6173  eloprabi  6186  riotass2  6332  riotass  6333  f1ocnvfv3  6340  riotasvdOLD  6348  riotasv3d  6353  riotasv3dOLD  6354  smoiso  6379  seqomlem4  6465  omopth2  6582  eqer  6693  uniqs  6719  mapsncnv  6814  ixpiin  6842  undifixp  6852  mapsnf1o  6857  mapunen  7030  ssenen  7035  pssnn  7081  en1eqsn  7088  findcard2  7098  unblem2  7110  domunfican  7129  fofinf1o  7137  f1opwfi  7159  marypha1lem  7186  ixpiunwdom  7305  infdifsn  7357  oemapwe  7396  rankpwi  7495  rankuni  7535  cardsucinf  7617  en2eqpr  7637  iunmapdisj  7650  infpwfien  7689  alephfp  7735  infmap2  7844  ackbij1lem16  7861  ackbij2  7869  cfsuc  7883  cfss  7891  enfin2i  7947  fin23lem22  7953  fin1a2lem6  8031  fin1a2lem11  8036  axcc2lem  8062  axcclem  8083  iundom2g  8162  ficard  8187  konigthlem  8190  fpwwe2lem8  8259  fpwwe2lem13  8264  fpwwe2  8265  canth4  8269  pwfseqlem4  8284  winalim2  8318  addassnq  8582  mulassnq  8583  distrnq  8585  ltsonq  8593  lterpq  8594  1idpr  8653  recexsrlem  8725  le2tri3i  8949  mul02lem2  8989  subdi  9213  infm3lem  9712  supmul1  9719  cru  9738  nn0ge0  9991  elz2  10040  zaddcl  10059  zindd  10113  xmulge0  10604  xadddi2  10617  prunioo  10764  fseq1p1m1  10857  fzrevral  10866  fllelt  10929  flval2  10944  modcyc  10999  uzrdgsuci  11023  fzen2  11031  axdc4uzlem  11044  seqf1olem1  11085  seqf1olem2  11086  sersub  11089  expgt1  11140  leexp2r  11159  sq01  11223  modexp  11236  bcm1k  11327  hashprg  11368  hashssdif  11374  hashmap  11387  hashbc  11391  hashf1lem1  11393  hashf1lem2  11394  swrds1  11473  shftlem  11563  shftfval  11565  replim  11601  cjexp  11635  sqrlem2  11729  sqrlem7  11734  resqrthlem  11740  abssq  11791  recan  11820  sqrthlem  11846  climmpt  12045  fsumcvg  12185  fsumcom2  12237  fsumconst  12252  fsumless  12254  cvgcmpce  12276  abscvgcvg  12277  incexclem  12295  isumsplit  12299  climcndslem1  12308  arisum  12318  geoserg  12324  geo2sum  12329  mertenslem1  12340  mertenslem2  12341  efcj  12373  efsub  12380  eflegeo  12401  sinneg  12426  cosneg  12427  sin01bnd  12465  cos01bnd  12466  divalgmod  12605  bitsinv1  12633  bitsf1ocnv  12635  sadadd2lem2  12641  gcdneg  12705  bezoutlem1  12717  bezoutlem3  12719  dvdssq  12739  isprm2lem  12765  isprm5  12791  divnumden  12819  zgcdsq  12824  phibnd  12839  pythagtriplem19  12886  iserodd  12888  pcprendvds2  12894  pczpre  12900  prmreclem1  12963  prmreclem4  12966  4sqlem4  12999  prmlem0  13107  strfvi  13186  topnval  13339  prdssca  13356  imasbas  13415  imasvscafn  13439  mrieqvlemd  13531  mrissmrcd  13542  catideu  13577  subcid  13721  funcres  13770  fucbas  13834  fuchom  13835  resssetc  13924  resscatc  13937  catcisolem  13938  xpcbas  13952  yonffthlem  14056  pospo  14107  lubprop  14114  glbprop  14119  acsinfdimd  14285  ismgmid2  14390  mndfo  14397  prds0g  14406  0mhm  14435  pwspjmhm  14444  gsumvallem1  14448  gsumval2a  14459  gsumccat  14464  gsumwmhm  14467  gsumwspan  14468  frmdval  14473  grpidd2  14519  grpinvid2  14531  grpnpcan  14557  grpsubsub4  14558  mulgfvi  14571  divsgrp2  14613  divs0  14675  ghmid  14689  ghminv  14690  gicsubgen  14742  gafo  14750  orbsta  14767  symgid  14781  cntrval  14795  oppgmnd  14827  oppginv  14832  mndodcong  14857  odval2  14866  odeq1  14873  odf1o1  14883  odf1o2  14884  odhash3  14887  gexdvds  14895  sylow2alem2  14929  lsmelvalm  14962  lsmmod2  14985  pj1lid  15010  pj1rid  15011  efginvrel2  15036  efgredleme  15052  efgredlemc  15054  efgredlemb  15055  efgrelexlemb  15059  frgp0  15069  lt6abl  15181  gsumzaddlem  15203  gsumcom2  15226  dprdfcntz  15250  dprdf1o  15267  dprd2da  15277  dpjrid  15297  pgpfac1lem3a  15311  pgpfaclem1  15316  ablfaclem3  15322  mgpress  15336  rnglz  15377  rngrz  15378  rngnegl  15380  rngnegr  15381  prdsmgp  15393  imasrng  15402  divsrng2  15403  opprrng  15413  crngunit  15444  issrngd  15626  lmod0vs  15663  islss3  15716  lspsn  15759  lmodindp1  15771  lmodvsinv2  15794  0lmhm  15797  invlmhm  15799  lmhmf1o  15803  pwsdiaglmhm  15814  lspsntrim  15851  lspabs2  15873  lspabs3  15874  lspexch  15882  lpi0  15999  lpi1  16000  ressmplbas2  16199  mplcoe3  16210  mplcoe2  16211  mplmon2  16234  ply1basfvi  16319  coe1subfv  16343  coe1tmmul2  16352  zndvds  16503  znf1o  16505  cygznlem3  16523  ipsubdir  16546  ipsubdi  16547  pjdm2  16611  pjf2  16614  toponcom  16668  tgtopon  16709  indistopon  16738  clsval2  16787  opncldf1  16821  mretopd  16829  toponmre  16830  restopnb  16906  ordtcnv  16931  lecldbas  16949  ordtrestixx  16952  iscncl  16998  cnprest  17017  pnrmopn  17071  ordtt1  17107  2ndcctbss  17181  kgenval  17230  elptr  17268  ptunimpt  17290  ptpjopn  17306  ptcld  17307  hausdiag  17339  qtopeu  17407  pt1hmeo  17497  ptuncnv  17498  ptunhmeo  17499  qtophmeo  17508  ufileu  17614  elfm3  17645  rnelfmlem  17647  fmfnfmlem3  17651  flffval  17684  isfcls  17704  ptcmplem5  17750  prdstmdd  17806  prdstgpd  17807  blfval  17947  setsms  18026  imasf1oxms  18035  stdbdmopn  18064  isngp4  18133  nmrtri  18145  nminvr  18180  lssnlm  18211  cnmet  18281  metds0  18354  metdstri  18355  metdseq0  18358  xrhmeo  18444  icccvx  18448  pcoass  18522  pcorevlem  18524  pcophtb  18527  elpi1i  18544  pi1xfr  18553  pi1xfrcnvlem  18554  lmhmclm  18584  clmmulg  18591  zlmclm  18593  clmzlmvsca  18594  tchcph  18667  cmetss  18740  pmltpclem2  18809  elovolmr  18835  iundisj2  18906  voliunlem1  18907  iunmbl2  18914  ioombl1lem4  18918  uniioombllem3  18940  uniioombllem4  18941  uniioombllem6  18943  dyadmaxlem  18952  volivth  18962  vitalilem3  18965  mbfsub  19017  mbfsup  19019  itg1addlem4  19054  itg1mulc  19059  mbfi1fseqlem6  19075  itgfsum  19181  itgsplitioo  19192  dvaddf  19291  dvexp  19302  dvcnvlem  19323  dvexp3  19325  dveflem  19326  rolle  19337  dvlip  19340  lhop1lem  19360  dvfsumlem1  19373  dvfsumlem3  19375  tdeglem4  19446  tdeglem2  19447  deg1suble  19493  ply1divalg2  19524  facth1  19550  fta1glem1  19551  dvply2g  19665  plydivlem3  19675  fta1lem  19687  quotcan  19689  aaliou3lem7  19729  aaliou3  19731  dvntaylp  19750  ulm2  19764  ulmclm  19766  mtest  19781  mbfulm  19782  pserulm  19798  abelthlem3  19809  abelthlem8  19815  reeff1o  19823  coseq0negpitopi  19871  abssinper  19886  sineq0  19889  cosord  19894  efiarg  19961  logdivlt  19972  logcnlem4  19992  logtayl  20007  dvcxp1  20082  dvcxp2  20083  sqrcn  20090  cxpeq  20097  ang180lem2  20108  ang180lem3  20109  logrec  20117  isosctrlem2  20119  isosctrlem3  20120  angpieqvd  20128  dcubic2  20140  cubic2  20144  dquartlem2  20148  dquart  20149  asinlem3  20167  atans2  20227  rlimcnp  20260  rlimcnp2  20261  amgmlem  20284  ftalem5  20314  dvdsppwf1o  20426  sgmmul  20440  perfect  20470  bcmono  20516  efexple  20520  bposlem1  20523  bposlem9  20531  lgsvalmod  20554  lgsneg  20558  lgsdchrval  20586  lgsquadlem1  20593  lgsquadlem2  20594  chtppilimlem1  20622  rpvmasumlem  20636  dchrisumlema  20637  dchrisumlem2  20639  dchrmusum2  20643  dchrvmasumlem1  20644  dchrvmasum2lem  20645  dchrvmasum2if  20646  dchrvmasumiflem1  20650  dchrisum0fmul  20655  dchrisum0lem2  20667  rplogsum  20676  selberg2lem  20699  logdivbnd  20705  pntrsumo1  20714  selberg3r  20718  selberg4r  20719  selberg34r  20720  pntrlog2bndlem2  20727  pntrlog2bndlem4  20729  qrngdiv  20773  isgrpo  20863  isgrpoi  20865  grpoidinvlem2  20872  grpoinvid2  20898  grpoinvf  20907  isgrpda  20964  subgoinv  20975  exidu1  20993  cmpidelt  20996  ablomul  21022  rngoideu  21051  rngo2  21055  rngolz  21068  rngorz  21069  rngmgmbs4  21084  rngorn1eq  21087  rngosn3  21093  nvmtri2  21238  dipcj  21290  sspg  21304  ssps  21306  sspn  21312  nmlno0lem  21371  cncph  21397  ipasslem2  21410  siii  21431  ubthlem1  21449  ubthlem2  21450  hlipcj  21490  hiidge0  21677  bcseqi  21699  shuni  21879  shunssi  21947  pjhthlem2  21971  shlub  21993  pjop  22006  pjpo  22007  h1de2i  22132  fh1  22197  fh2  22198  chscllem2  22217  chscllem3  22218  pjo  22250  pjcji  22263  hmopre  22503  adjvalval  22517  hmopadj  22519  hmoplin  22522  idhmop  22562  nmlnop0iALT  22575  nmopun  22594  cnvbraval  22690  bracnlnval  22694  kbass3  22698  pjhmopi  22726  hstoh  22812  sto2i  22817  atom1d  22933  atcv0eq  22959  atcv1  22960  ifeqeqx  23034  ballotlemfp1  23050  ballotlemsf1o  23072  ballotlemrinv0  23091  difeq  23128  ifbieq12d2  23149  fimacnvinrn  23199  fmptcof2  23229  xlt2addrd  23253  xrge0pluscn  23322  iundisj2fi  23364  iundisj2f  23366  logbrec  23407  esumval  23425  esumel  23426  esumc  23430  esumpfinvallem  23442  esumpcvgval  23446  esumpmono  23447  esumcocn  23448  unisg  23504  indf1ofs  23609  probmeasb  23633  zetacvg  23689  subfacp1lem5  23715  subfacval2  23718  subfacval3  23720  conpcon  23766  sconpi1  23770  umgraex  23875  eupath2  23904  relexpcnv  24029  relexpadd  24035  rtrclreclem.trans  24043  dfrtrcl2  24045  tfisg  24204  wfr3g  24255  tfr3ALT  24279  frr3g  24280  nofnbday  24306  sltres  24318  nodense  24343  colinearalglem2  24535  ax5seglem9  24565  axpaschlem  24568  axpasch  24569  axcontlem7  24598  fvtransport  24655  transportprops  24657  btwnconn1lem12  24721  midofsegid  24727  outsideofeq  24753  lineunray  24770  bpolysum  24788  fsumcube  24795  rankeq1o  24801  onsuctopon  24873  areacirclem2  24925  areacirclem5  24929  moec  25047  domrngref  25060  domfldref  25061  cnvref2  25066  mapex2  25140  repfuntw  25160  cbicp  25166  prl2  25169  valcurfn1  25204  sege  25252  mxlmnl2  25270  defse3  25272  supwval  25284  dffprod  25319  fprodp1  25323  iscom  25333  reacomsmgrp1  25343  reacomsmgrp2  25344  reacomsmgrp4  25346  resgcom  25351  trran2  25393  ltrran2  25403  ltrooo  25404  ltrinvlem  25406  rltrran  25414  multinv  25422  multinvb  25423  addvecass  25465  dblsubvec  25474  mvecrtol2  25477  mulveczer  25479  mulinvsca  25480  svli2  25484  svs2  25487  svs3  25488  inttop4  25517  sallnei  25529  intopcoaconlem3b  25538  intopcoaconlem3  25539  mslb1  25607  2wsms  25608  trran  25614  supnuf  25629  addcanrg  25667  negveud  25668  negveudr  25669  mulmulvec  25687  distsava  25689  dcsda  25733  1ded  25738  rcmob  25749  dmrngcmp  25751  1cat  25759  morcat  25780  cmpassoh  25801  homgrf  25802  imonclem  25813  cmpmon  25815  icmpmon  25816  isfuna  25834  idfisf  25841  idsubidsup  25857  idsubfun  25858  vtarl  25887  rocatval  25959  cmp2morpcats  25961  cmpmorass  25966  morexcmp2  25968  cmpidmor3  25970  cmppar3  25974  segline  26141  bhp3  26177  nn0prpwlem  26238  opnbnd  26243  cldbnd  26244  refssfne  26294  fnejoin2  26318  sdclem2  26452  trirn  26463  stiooOLD  26471  isbnd2  26507  ghomdiv  26574  rngogrphom  26602  0rngo  26652  prnc  26692  isdmn3  26699  prtlem11  26734  elrfi  26769  elrfirn  26770  mapfzcons  26793  mzprename  26827  eldioph2b  26842  lzenom  26849  diophin  26852  eq0rabdioph  26856  rexrabdioph  26875  rexzrexnn0  26885  fphpdo  26900  irrapxlem2  26908  irrapxlem3  26909  irrapxlem5  26911  pellexlem2  26915  pellexlem6  26919  pell1234qrdich  26946  pell14qrdich  26954  pell1qrge1  26955  pell1qrgaplem  26958  pellfund14gap  26972  qirropth  26993  rmxyelqirr  26995  rmxycomplete  27002  rmxy1  27007  rmym1  27020  rmxluc  27021  rmxdbl  27024  acongtr  27065  jm2.18  27081  jm2.22  27088  jm2.23  27089  jm2.25  27092  jm2.26lem3  27094  jm2.27a  27098  jm2.27c  27100  fnwe2lem3  27149  kelac1  27161  pwssplit4  27191  filnm  27192  pwslnmlem2  27195  frlmpws  27218  frlmlss  27219  frlmlbs  27249  frlmup3  27252  ellspd  27254  unxpwdom3  27256  imasgim  27264  isnumbasgrplem3  27270  lsslindf  27300  islindf4  27308  islindf5  27309  hbt  27334  mpaaeu  27355  rngunsnply  27378  en2eleq  27381  pmtrfrn  27400  psgnunilem1  27416  hashgcdlem  27516  proot1ex  27520  ofdivrec  27543  iotaexeu  27618  iotasbc  27619  pm14.24  27632  sbiota1  27634  cncmpmax  27703  refsum2cnlem1  27708  cncfmptss  27717  expcnfg  27726  clim1fr1  27727  isumneg  27728  climexp  27731  climneg  27736  climdivf  27738  itgsin0pilem1  27744  ibliccsinexp  27745  itgsinexplem1  27748  itgsinexp  27749  stoweidlem1  27750  stoweidlem2  27751  stoweidlem3  27752  stoweidlem11  27760  stoweidlem13  27762  stoweidlem19  27768  stoweidlem21  27770  stoweidlem24  27773  stoweidlem26  27775  stoweidlem29  27778  stoweidlem40  27789  stoweidlem42  27791  stoweidlem55  27804  stoweidlem59  27808  stoweidlem62  27811  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  stirlinglem1  27823  stirlinglem3  27825  stirlinglem4  27826  stirlinglem5  27827  stirlinglem6  27828  stirlinglem7  27829  stirlinglem8  27830  stirlinglem10  27832  stirlinglem11  27833  stirlinglem12  27834  stirlinglem15  27837  sigaras  27845  sigarms  27846  sigarperm  27850  sharhght  27855  afvelrn  28030  afvres  28034  dmfcoafv  28036  afvco2  28037  difprsneq  28068  difprsng  28069  diftpsneq  28070  mpt2xopoveqd  28087  elprchashprn2  28088  s4f1o  28093  nbgraop  28140  uvtxnbgra  28165  onetansqsecsq  28231  csbsngVD  28669  bnj1241  28840  bnj548  28929  lsatel  29195  lsatfixedN  29199  lsat0cv  29223  ldualgrplem  29335  lduallmodlem  29342  lkrpssN  29353  lkreqN  29360  omlfh1N  29448  atcvreq0  29504  glbconN  29566  2atjm  29634  hlatexch3N  29669  lplnexllnN  29753  2llnjaN  29755  2lplnja  29808  dalem56  29917  2llnma1b  29975  atmod1i1  30046  atmod1i2  30048  llnmod1i2  30049  dalawlem11  30070  pclfinN  30089  osumclN  30156  4atexlemswapqr  30252  4atexlemunv  30255  cdleme15a  30463  cdleme16  30474  cdleme22cN  30531  cdleme22d  30532  cdleme43dN  30681  cdlemeg46sfg  30709  cdlemeg46fjgN  30710  cdlemg1a  30759  cdlemeiota  30774  cdlemg3a  30786  cdlemg12e  30836  cdlemg18a  30867  trlcone  30917  tgrpgrplem  30938  tgrpabl  30940  cdlemk4  31023  cdlemksv2  31036  cdlemkuv2  31056  cdlemk19  31058  cdlemk22  31082  cdlemk53a  31144  erngdvlem1  31177  erngdvlem2N  31178  erngdvlem3  31179  erngdvlem4  31180  erngdvlem1-rN  31185  erngdvlem2-rN  31186  erngdvlem3-rN  31187  erngdvlem4-rN  31188  dvalveclem  31215  dialss  31236  dia2dimlem2  31255  dia2dimlem3  31256  dvhgrp  31297  dvhlveclem  31298  cdlemm10N  31308  doca2N  31316  diblss  31360  dicvaddcl  31380  dicvscacl  31381  dicn0  31382  diclss  31383  cdlemn11a  31397  dihjust  31407  dihopelvalcpre  31438  dihmeetlem5  31498  dochlkr  31575  dihsmatrn  31626  dvh4dimat  31628  mapdval4N  31822  mapdcv  31850  mapdpglem15  31876  baerlem5bmN  31907  baerlem5abmN  31908  mapdh8aa  31966  hdmapval3lemN  32030  hdmap10lem  32032  hdmaprnlem10N  32052  hdmap14lem2a  32060  hdmap14lem2N  32062  hdmap14lem3  32063  hdmap14lem6  32066  hgmapvs  32084  hlhilocv  32150  hlhillcs  32151
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator