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

Theorem eqcomd 2409
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 2406 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2sylib 189 1  |-  ( ph  ->  B  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  eqtr2d  2437  eqtr3d  2438  eqtr4d  2439  syl5req  2449  syl6req  2453  sylan9req  2457  eqeltrrd  2479  eleqtrrd  2481  syl5eleqr  2491  syl6eqelr  2493  eqnetrrd  2587  neeqtrrd  2591  dedhb  3064  eqsstr3d  3343  sseqtr4d  3345  syl6eqssr  3359  dfrab3ss  3579  uneqdifeq  3676  ifbi  3716  ifbothda  3729  dedth  3740  elimhyp  3747  elimhyp2v  3748  elimhyp3v  3749  elimhyp4v  3750  elimdhyp  3752  keephyp2v  3754  keephyp3v  3755  disjsn2  3829  diftpsn3  3897  unimax  4009  iununi  4135  sndisj  4164  disjprg  4168  eqbrtrrd  4194  breqtrrd  4198  syl5breqr  4208  syl6eqbrr  4210  class2seteq  4328  opth1  4394  euotd  4417  opelopabsb  4425  ordsuc  4753  tfisi  4797  0nelxp  4865  opeliunxp  4888  sosn  4906  somincom  5230  iotaex  5394  iota4  5395  fun2ssres  5453  funimass1  5485  funssfv  5705  fnimapr  5746  fvun  5752  fmptco  5860  fnpr  5909  fnprOLD  5910  foeqcnvco  5986  f1eqcocnv  5987  f1oiso2  6031  f1opw2  6257  sbcopeq1a  6358  csbopeq1a  6359  eloprabi  6372  f2ndf  6411  mpt2xopoveqd  6431  riotass2  6536  riotass  6537  f1ocnvfv3  6544  riotasvdOLD  6552  riotasv3d  6557  riotasv3dOLD  6558  smoiso  6583  seqomlem4  6669  omopth2  6786  eqer  6897  uniqs  6923  mapsncnv  7019  ixpiin  7047  undifixp  7057  mapsnf1o  7062  mapunen  7235  ssenen  7240  pssnn  7286  en1eqsn  7297  findcard2  7307  unblem2  7319  domunfican  7338  fofinf1o  7346  f1opwfi  7368  inelfi  7381  marypha1lem  7396  ixpiunwdom  7515  infdifsn  7567  oemapwe  7606  rankpwi  7705  rankuni  7745  cardsucinf  7827  en2eqpr  7847  iunmapdisj  7860  infpwfien  7899  alephfp  7945  infmap2  8054  ackbij1lem16  8071  ackbij2  8079  cfsuc  8093  cfss  8101  enfin2i  8157  fin23lem22  8163  fin1a2lem6  8241  fin1a2lem11  8246  axcc2lem  8272  axcclem  8293  iundom2g  8371  ficard  8396  konigthlem  8399  fpwwe2lem8  8468  fpwwe2lem13  8473  fpwwe2  8474  canth4  8478  pwfseqlem4  8493  winalim2  8527  addassnq  8791  mulassnq  8792  distrnq  8794  ltsonq  8802  lterpq  8803  1idpr  8862  recexsrlem  8934  le2tri3i  9159  mul02lem2  9199  subdi  9423  infm3lem  9922  supmul1  9929  cru  9948  nn0ge0  10203  elz2  10254  zaddcl  10273  zindd  10327  xmulge0  10819  xadddi2  10832  prunioo  10981  fseq1p1m1  11077  fzrevral  11086  injresinj  11155  fllelt  11161  flval2  11176  modcyc  11231  uzrdgsuci  11255  fzen2  11263  axdc4uzlem  11276  seqf1olem1  11317  seqf1olem2  11318  sersub  11321  expgt1  11373  leexp2r  11392  sq01  11456  modexp  11469  bcm1k  11561  bcn2m1  11570  hashunx  11615  hashprg  11621  elprchashprn2  11622  hashssdif  11632  hashmap  11653  hashbc  11657  hashf1lem1  11659  hashf1lem2  11660  swrds1  11742  s4f1o  11820  shftlem  11838  shftfval  11840  replim  11876  cjexp  11910  sqrlem2  12004  sqrlem7  12009  resqrthlem  12015  abssq  12066  recan  12095  sqrthlem  12121  climmpt  12320  fsumcvg  12461  fsumcom2  12513  fsumconst  12528  fsumless  12530  cvgcmpce  12552  abscvgcvg  12553  incexclem  12571  isumsplit  12575  climcndslem1  12584  arisum  12594  geoserg  12600  geo2sum  12605  mertenslem1  12616  mertenslem2  12617  efcj  12649  efsub  12656  eflegeo  12677  sinneg  12702  cosneg  12703  sin01bnd  12741  cos01bnd  12742  divalgmod  12881  bitsinv1  12909  bitsf1ocnv  12911  gcdneg  12981  bezoutlem1  12993  bezoutlem3  12995  dvdssq  13015  isprm2lem  13041  isprm5  13067  divnumden  13095  zgcdsq  13100  phibnd  13115  pythagtriplem19  13162  iserodd  13164  pcprendvds2  13170  pczpre  13176  prmreclem1  13239  prmreclem4  13242  4sqlem4  13275  prmlem0  13383  strfvi  13462  topnval  13617  prdssca  13634  imasbas  13693  imasvscafn  13717  mrieqvlemd  13809  mrissmrcd  13820  catideu  13855  subcid  13999  funcres  14048  fucbas  14112  fuchom  14113  resssetc  14202  resscatc  14215  catcisolem  14216  xpcbas  14230  yonffthlem  14334  pospo  14385  lubprop  14392  glbprop  14397  acsinfdimd  14563  ismgmid2  14668  mndfo  14675  prds0g  14684  0mhm  14713  pwspjmhm  14722  gsumvallem1  14726  gsumval2a  14737  gsumccat  14742  gsumwmhm  14745  gsumwspan  14746  frmdval  14751  grpidd2  14797  grpinvid2  14809  grpnpcan  14835  grpsubsub4  14836  mulgfvi  14849  divsgrp2  14891  divs0  14953  ghmid  14967  ghminv  14968  gicsubgen  15020  gafo  15028  orbsta  15045  symgid  15059  cntrval  15073  oppgmnd  15105  oppginv  15110  mndodcong  15135  odval2  15144  odeq1  15151  odf1o1  15161  odf1o2  15162  odhash3  15165  gexdvds  15173  sylow2alem2  15207  lsmelvalm  15240  lsmmod2  15263  pj1lid  15288  pj1rid  15289  efginvrel2  15314  efgredleme  15330  efgredlemc  15332  efgredlemb  15333  efgrelexlemb  15337  frgp0  15347  lt6abl  15459  gsumzaddlem  15481  gsumcom2  15504  dprdfcntz  15528  dprdf1o  15545  dprd2da  15555  dpjrid  15575  pgpfac1lem3a  15589  pgpfaclem1  15594  ablfaclem3  15600  mgpress  15614  rnglz  15655  rngrz  15656  rngnegl  15658  rngnegr  15659  prdsmgp  15671  imasrng  15680  divsrng2  15681  opprrng  15691  crngunit  15722  issrngd  15904  lmod0vs  15938  islss3  15990  lspsn  16033  lmodindp1  16045  lmodvsinv2  16068  0lmhm  16071  invlmhm  16073  lmhmf1o  16077  pwsdiaglmhm  16088  lspsntrim  16125  lspabs2  16147  lspabs3  16148  lspexch  16156  lpi0  16273  lpi1  16274  ressmplbas2  16473  mplcoe3  16484  mplcoe2  16485  mplmon2  16508  ply1basfvi  16590  coe1subfv  16614  coe1tmmul2  16623  zndvds  16785  znf1o  16787  cygznlem3  16805  ipsubdir  16828  ipsubdi  16829  pjdm2  16893  pjf2  16896  toponcom  16950  tgtopon  16991  indistopon  17020  clsval2  17069  opncldf1  17103  mretopd  17111  toponmre  17112  neiptopuni  17149  neiptopreu  17152  restopnb  17193  ordtcnv  17219  lecldbas  17237  ordtrestixx  17240  iscncl  17287  cnprest  17307  pnrmopn  17361  ordtt1  17397  2ndcctbss  17471  kgenval  17520  elptr  17558  ptunimpt  17580  ptpjopn  17597  ptcld  17598  hausdiag  17630  qtopeu  17701  pt1hmeo  17791  ptuncnv  17792  ptunhmeo  17793  qtophmeo  17802  ufileu  17904  elfm3  17935  rnelfmlem  17937  fmfnfmlem3  17941  flffval  17974  isfcls  17994  ptcmplem5  18040  prdstmdd  18106  prdstgpd  18107  utopbas  18218  restutopopn  18221  ustuqtop1  18224  ustuqtop3  18226  ustuqtop5  18228  blfvalps  18366  setsms  18463  imasf1oxms  18472  stdbdmopn  18501  isngp4  18611  nmrtri  18623  nminvr  18658  lssnlm  18689  cnmet  18759  metds0  18833  metdstri  18834  metdseq0  18837  xrhmeo  18924  icccvx  18928  pcoass  19002  pcorevlem  19004  pcophtb  19007  elpi1i  19024  pi1xfr  19033  pi1xfrcnvlem  19034  lmhmclm  19064  clmmulg  19071  zlmclm  19073  clmzlmvsca  19074  tchcph  19147  cmetss  19220  pmltpclem2  19299  elovolmr  19325  iundisj2  19396  voliunlem1  19397  iunmbl2  19404  ioombl1lem4  19408  uniioombllem3  19430  uniioombllem4  19431  uniioombllem6  19433  dyadmaxlem  19442  volivth  19452  vitalilem3  19455  mbfsub  19507  mbfsup  19509  itg1addlem4  19544  itg1mulc  19549  mbfi1fseqlem6  19565  itgfsum  19671  itgsplitioo  19682  dvaddf  19781  dvexp  19792  dvcnvlem  19813  dvexp3  19815  dveflem  19816  rolle  19827  dvlip  19830  lhop1lem  19850  dvfsumlem1  19863  dvfsumlem3  19865  tdeglem4  19936  tdeglem2  19937  deg1suble  19983  ply1divalg2  20014  facth1  20040  fta1glem1  20041  dvply2g  20155  plydivlem3  20165  fta1lem  20177  quotcan  20179  aaliou3lem7  20219  aaliou3  20221  dvntaylp  20240  ulm2  20254  ulmclm  20256  ulmuni  20261  mtest  20273  mbfulm  20275  pserulm  20291  abelthlem3  20302  abelthlem8  20308  reeff1o  20316  coseq0negpitopi  20364  abssinper  20379  sineq0  20382  cosord  20387  efiarg  20455  abslogle  20466  logdivlt  20469  logcnlem4  20489  logtayl  20504  dvcxp1  20579  dvcxp2  20580  sqrcn  20587  cxpeq  20594  ang180lem2  20605  ang180lem3  20606  logrec  20614  isosctrlem2  20616  isosctrlem3  20617  angpieqvd  20625  dcubic2  20637  cubic2  20641  dquartlem2  20645  dquart  20646  asinlem3  20664  atans2  20724  rlimcnp  20757  rlimcnp2  20758  amgmlem  20781  ftalem5  20812  dvdsppwf1o  20924  sgmmul  20938  perfect  20968  bcmono  21014  efexple  21018  bposlem1  21021  bposlem9  21029  lgsvalmod  21052  lgsneg  21056  lgsdchrval  21084  lgsquadlem2  21092  chtppilimlem1  21120  rpvmasumlem  21134  dchrisumlema  21135  dchrisumlem2  21137  dchrmusum2  21141  dchrvmasumlem1  21142  dchrvmasum2lem  21143  dchrvmasum2if  21144  dchrvmasumiflem1  21148  dchrisum0fmul  21153  dchrisum0lem2  21165  rplogsum  21174  selberg2lem  21197  logdivbnd  21203  pntrsumo1  21212  selberg3r  21216  selberg4r  21217  selberg34r  21218  pntrlog2bndlem2  21225  pntrlog2bndlem4  21227  qrngdiv  21271  umgraex  21311  nbgraop  21389  cusgrasizeinds  21438  cusgrasize2inds  21439  cusgrafilem2  21442  uvtxnbgra  21455  0wlkon  21500  redwlk  21559  fargshiftlem  21574  fargshiftfo  21578  fargshiftfva  21579  dfconngra1  21611  eupatrl  21643  eupath2  21655  isgrpo  21737  isgrpoi  21739  grpoidinvlem2  21746  grpoinvid2  21772  grpoinvf  21781  isgrpda  21838  subgoinv  21849  exidu1  21867  cmpidelt  21870  ablomul  21896  rngoideu  21925  rngo2  21929  rngolz  21942  rngorz  21943  rngmgmbs4  21958  rngorn1eq  21961  rngosn3  21967  nvmtri2  22114  dipcj  22166  sspg  22180  ssps  22182  sspn  22188  nmlno0lem  22247  cncph  22273  ipasslem2  22286  siii  22307  ubthlem1  22325  ubthlem2  22326  hlipcj  22366  hiidge0  22553  bcseqi  22575  shuni  22755  shunssi  22823  pjhthlem2  22847  shlub  22869  pjop  22882  pjpo  22883  h1de2i  23008  fh1  23073  fh2  23074  chscllem2  23093  chscllem3  23094  pjo  23126  pjcji  23139  hmopre  23379  adjvalval  23393  hmopadj  23395  hmoplin  23398  idhmop  23438  nmlnop0iALT  23451  nmopun  23470  cnvbraval  23566  bracnlnval  23570  kbass3  23574  pjhmopi  23602  hstoh  23688  sto2i  23693  atom1d  23809  atcv0eq  23835  atcv1  23836  ifeqeqx  23954  ifbieq12d2  23955  iundisj2f  23983  imadifxp  23991  ofresid  24008  fmptcof2  24029  xlt2addrd  24077  iundisj2fi  24106  ofldchr  24197  redvr  24230  xrge0pluscn  24279  qqhval2lem  24318  qqhval2  24319  rrhcn  24333  logbrec  24358  indf1ofs  24376  esumel  24395  esumc  24399  gsumesum  24404  esumfsup  24413  esumfsupre  24414  esumpfinvallem  24417  esumpcvgval  24421  esumpmono  24422  esumcocn  24423  unisg  24479  voliune  24538  volfiniune  24539  probmeasb  24641  ballotlemfp1  24702  ballotlemsf1o  24724  ballotlemrinv0  24743  zetacvg  24752  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamcvg2  24792  gamcvg2lem  24796  subfacp1lem5  24823  subfacval2  24826  subfacval3  24828  conpcon  24875  sconpi1  24879  relexpcnv  25086  relexpadd  25091  rtrclreclem.trans  25099  dfrtrcl2  25101  clim2div  25170  fprodcvg  25209  fprodss  25227  fprodser  25228  fprodconst  25255  fprodcom2  25261  iprodfac  25314  tfisg  25418  wfr3g  25469  tfr3ALT  25493  frr3g  25494  nofnbday  25520  sltres  25532  nodense  25557  colinearalglem2  25750  ax5seglem9  25780  axpaschlem  25783  axpasch  25784  axcontlem7  25813  fvtransport  25870  transportprops  25872  btwnconn1lem12  25936  midofsegid  25942  outsideofeq  25968  lineunray  25985  bpolysum  26003  fsumcube  26010  rankeq1o  26016  onsuctopon  26088  supaddc  26137  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  itg2addnclem  26155  itg2addnc  26158  areacirclem2  26181  areacirclem5  26185  nn0prpwlem  26215  opnbnd  26218  cldbnd  26219  refssfne  26264  fnejoin2  26288  sdclem2  26336  trirn  26347  isbnd2  26382  ghomdiv  26449  rngogrphom  26477  0rngo  26527  prnc  26567  isdmn3  26574  prtlem11  26605  elrfi  26638  elrfirn  26639  mapfzcons  26662  mzprename  26696  eldioph2b  26711  lzenom  26718  diophin  26721  eq0rabdioph  26725  rexrabdioph  26744  rexzrexnn0  26754  fphpdo  26768  irrapxlem2  26776  irrapxlem3  26777  irrapxlem5  26779  pellexlem2  26783  pellexlem6  26787  pell1234qrdich  26814  pell14qrdich  26822  pell1qrge1  26823  pell1qrgaplem  26826  pellfund14gap  26840  qirropth  26861  rmxyelqirr  26863  rmxycomplete  26870  rmxy1  26875  rmym1  26888  rmxluc  26889  rmxdbl  26892  acongtr  26933  jm2.18  26949  jm2.22  26956  jm2.23  26957  jm2.25  26960  jm2.26lem3  26962  jm2.27a  26966  jm2.27c  26968  fnwe2lem3  27017  kelac1  27029  pwssplit4  27059  filnm  27060  pwslnmlem2  27063  frlmpws  27086  frlmlss  27087  frlmlbs  27117  frlmup3  27120  ellspd  27122  unxpwdom3  27124  imasgim  27132  isnumbasgrplem3  27138  lsslindf  27168  islindf4  27176  islindf5  27177  hbt  27202  mpaaeu  27223  rngunsnply  27246  en2eleq  27249  pmtrfrn  27268  psgnunilem1  27284  hashgcdlem  27384  proot1ex  27388  ofdivrec  27411  iotaexeu  27486  iotasbc  27487  pm14.24  27500  sbiota1  27502  cncmpmax  27570  refsum2cnlem1  27575  expcnfg  27593  clim1fr1  27594  isumneg  27595  climneg  27603  climdivf  27605  itgsin0pilem1  27611  ibliccsinexp  27612  itgsinexplem1  27615  itgsinexp  27616  stoweidlem2  27618  stoweidlem3  27619  stoweidlem13  27629  stoweidlem19  27635  stoweidlem21  27637  stoweidlem24  27640  stoweidlem26  27642  stoweidlem29  27645  stoweidlem40  27656  stoweidlem42  27658  stoweidlem62  27678  wallispilem4  27684  wallispi  27686  wallispi2lem1  27687  wallispi2lem2  27688  stirlinglem1  27690  stirlinglem3  27692  stirlinglem4  27693  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem8  27697  stirlinglem10  27699  stirlinglem12  27701  stirlinglem15  27704  sigaras  27712  sigarms  27713  sigarperm  27717  sharhght  27722  afvelrn  27899  afvres  27903  dmfcoafv  27906  afvco2  27907  2if2  27941  resisresindm  27957  imarnf1pr  27965  fzosplitsnm1  27991  swrd0swrd  28009  swrdswrd  28011  swrdswrd0  28013  swrdccatin12lem3b  28022  swrdccatin12lem3  28024  swrdccat3b  28031  usgra2adedgwlk  28046  usg2spthonot  28085  usg2spthonot0  28086  frgraunss  28099  frgrancvvdeqlem4  28136  frg2woteq  28163  onetansqsecsq  28218  csbsngVD  28714  bnj1241  28885  bnj548  28974  lsatel  29488  lsatfixedN  29492  lsat0cv  29516  ldualgrplem  29628  lduallmodlem  29635  lkrpssN  29646  lkreqN  29653  omlfh1N  29741  atcvreq0  29797  glbconN  29859  2atjm  29927  hlatexch3N  29962  lplnexllnN  30046  2llnjaN  30048  2lplnja  30101  dalem56  30210  2llnma1b  30268  atmod1i1  30339  atmod1i2  30341  llnmod1i2  30342  dalawlem11  30363  pclfinN  30382  osumclN  30449  4atexlemswapqr  30545  4atexlemunv  30548  cdleme15a  30756  cdleme16  30767  cdleme22cN  30824  cdleme22d  30825  cdleme43dN  30974  cdlemeg46sfg  31002  cdlemeg46fjgN  31003  cdlemg1a  31052  cdlemeiota  31067  cdlemg3a  31079  cdlemg12e  31129  cdlemg18a  31160  trlcone  31210  tgrpgrplem  31231  tgrpabl  31233  cdlemk4  31316  cdlemksv2  31329  cdlemkuv2  31349  cdlemk19  31351  cdlemk22  31375  cdlemk53a  31437  erngdvlem1  31470  erngdvlem2N  31471  erngdvlem3  31472  erngdvlem4  31473  erngdvlem1-rN  31478  erngdvlem2-rN  31479  erngdvlem3-rN  31480  erngdvlem4-rN  31481  dvalveclem  31508  dialss  31529  dia2dimlem2  31548  dia2dimlem3  31549  dvhgrp  31590  dvhlveclem  31591  cdlemm10N  31601  doca2N  31609  diblss  31653  dicvaddcl  31673  dicvscacl  31674  dicn0  31675  diclss  31676  cdlemn11a  31690  dihjust  31700  dihopelvalcpre  31731  dihmeetlem5  31791  dochlkr  31868  dihsmatrn  31919  dvh4dimat  31921  mapdval4N  32115  mapdcv  32143  mapdpglem15  32169  baerlem5bmN  32200  baerlem5abmN  32201  mapdh8aa  32259  hdmapval3lemN  32323  hdmap10lem  32325  hdmaprnlem10N  32345  hdmap14lem2a  32353  hdmap14lem2N  32355  hdmap14lem3  32356  hdmap14lem6  32359  hgmapvs  32377  hlhilocv  32443  hlhillcs  32444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-cleq 2397
  Copyright terms: Public domain W3C validator