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

Theorem eqcomd 2301
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 2298 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2sylib 188 1  |-  ( ph  ->  B  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  eqtr2d  2329  eqtr3d  2330  eqtr4d  2331  syl5req  2341  syl6req  2345  sylan9req  2349  eqeltrrd  2371  eleqtrrd  2373  syl5eleqr  2383  syl6eqelr  2385  eqnetrrd  2479  neeqtrrd  2483  dedhb  2948  eqsstr3d  3226  sseqtr4d  3228  syl6eqssr  3242  dfrab3ss  3459  uneqdifeq  3555  ifbi  3595  ifbothda  3608  dedth  3619  elimhyp  3626  elimhyp2v  3627  elimhyp3v  3628  elimhyp4v  3629  elimdhyp  3631  keephyp2v  3633  keephyp3v  3634  disjsn2  3707  diftpsn3  3772  unimax  3877  iununi  4002  sndisj  4031  disjprg  4035  eqbrtrrd  4061  breqtrrd  4065  syl5breqr  4075  syl6eqbrr  4077  class2seteq  4195  opth1  4260  euotd  4283  opelopabsb  4291  ordsuc  4621  tfisi  4665  0nelxp  4733  opeliunxp  4756  sosn  4775  somincom  5096  iotaex  5252  iota4  5253  fun2ssres  5311  funimass1  5341  funssfv  5559  fnimapr  5599  fvun  5605  fmptco  5707  foeqcnvco  5820  f1eqcocnv  5821  f1oiso2  5865  f1opw2  6087  sbcopeq1a  6188  csbopeq1a  6189  eloprabi  6202  riotass2  6348  riotass  6349  f1ocnvfv3  6356  riotasvdOLD  6364  riotasv3d  6369  riotasv3dOLD  6370  smoiso  6395  seqomlem4  6481  omopth2  6598  eqer  6709  uniqs  6735  mapsncnv  6830  ixpiin  6858  undifixp  6868  mapsnf1o  6873  mapunen  7046  ssenen  7051  pssnn  7097  en1eqsn  7104  findcard2  7114  unblem2  7126  domunfican  7145  fofinf1o  7153  f1opwfi  7175  marypha1lem  7202  ixpiunwdom  7321  infdifsn  7373  oemapwe  7412  rankpwi  7511  rankuni  7551  cardsucinf  7633  en2eqpr  7653  iunmapdisj  7666  infpwfien  7705  alephfp  7751  infmap2  7860  ackbij1lem16  7877  ackbij2  7885  cfsuc  7899  cfss  7907  enfin2i  7963  fin23lem22  7969  fin1a2lem6  8047  fin1a2lem11  8052  axcc2lem  8078  axcclem  8099  iundom2g  8178  ficard  8203  konigthlem  8206  fpwwe2lem8  8275  fpwwe2lem13  8280  fpwwe2  8281  canth4  8285  pwfseqlem4  8300  winalim2  8334  addassnq  8598  mulassnq  8599  distrnq  8601  ltsonq  8609  lterpq  8610  1idpr  8669  recexsrlem  8741  le2tri3i  8965  mul02lem2  9005  subdi  9229  infm3lem  9728  supmul1  9735  cru  9754  nn0ge0  10007  elz2  10056  zaddcl  10075  zindd  10129  xmulge0  10620  xadddi2  10633  prunioo  10780  fseq1p1m1  10873  fzrevral  10882  fllelt  10945  flval2  10960  modcyc  11015  uzrdgsuci  11039  fzen2  11047  axdc4uzlem  11060  seqf1olem1  11101  seqf1olem2  11102  sersub  11105  expgt1  11156  leexp2r  11175  sq01  11239  modexp  11252  bcm1k  11343  hashprg  11384  hashssdif  11390  hashmap  11403  hashbc  11407  hashf1lem1  11409  hashf1lem2  11410  swrds1  11489  shftlem  11579  shftfval  11581  replim  11617  cjexp  11651  sqrlem2  11745  sqrlem7  11750  resqrthlem  11756  abssq  11807  recan  11836  sqrthlem  11862  climmpt  12061  fsumcvg  12201  fsumcom2  12253  fsumconst  12268  fsumless  12270  cvgcmpce  12292  abscvgcvg  12293  incexclem  12311  isumsplit  12315  climcndslem1  12324  arisum  12334  geoserg  12340  geo2sum  12345  mertenslem1  12356  mertenslem2  12357  efcj  12389  efsub  12396  eflegeo  12417  sinneg  12442  cosneg  12443  sin01bnd  12481  cos01bnd  12482  divalgmod  12621  bitsinv1  12649  bitsf1ocnv  12651  sadadd2lem2  12657  gcdneg  12721  bezoutlem1  12733  bezoutlem3  12735  dvdssq  12755  isprm2lem  12781  isprm5  12807  divnumden  12835  zgcdsq  12840  phibnd  12855  pythagtriplem19  12902  iserodd  12904  pcprendvds2  12910  pczpre  12916  prmreclem1  12979  prmreclem4  12982  4sqlem4  13015  prmlem0  13123  strfvi  13202  topnval  13355  prdssca  13372  imasbas  13431  imasvscafn  13455  mrieqvlemd  13547  mrissmrcd  13558  catideu  13593  subcid  13737  funcres  13786  fucbas  13850  fuchom  13851  resssetc  13940  resscatc  13953  catcisolem  13954  xpcbas  13968  yonffthlem  14072  pospo  14123  lubprop  14130  glbprop  14135  acsinfdimd  14301  ismgmid2  14406  mndfo  14413  prds0g  14422  0mhm  14451  pwspjmhm  14460  gsumvallem1  14464  gsumval2a  14475  gsumccat  14480  gsumwmhm  14483  gsumwspan  14484  frmdval  14489  grpidd2  14535  grpinvid2  14547  grpnpcan  14573  grpsubsub4  14574  mulgfvi  14587  divsgrp2  14629  divs0  14691  ghmid  14705  ghminv  14706  gicsubgen  14758  gafo  14766  orbsta  14783  symgid  14797  cntrval  14811  oppgmnd  14843  oppginv  14848  mndodcong  14873  odval2  14882  odeq1  14889  odf1o1  14899  odf1o2  14900  odhash3  14903  gexdvds  14911  sylow2alem2  14945  lsmelvalm  14978  lsmmod2  15001  pj1lid  15026  pj1rid  15027  efginvrel2  15052  efgredleme  15068  efgredlemc  15070  efgredlemb  15071  efgrelexlemb  15075  frgp0  15085  lt6abl  15197  gsumzaddlem  15219  gsumcom2  15242  dprdfcntz  15266  dprdf1o  15283  dprd2da  15293  dpjrid  15313  pgpfac1lem3a  15327  pgpfaclem1  15332  ablfaclem3  15338  mgpress  15352  rnglz  15393  rngrz  15394  rngnegl  15396  rngnegr  15397  prdsmgp  15409  imasrng  15418  divsrng2  15419  opprrng  15429  crngunit  15460  issrngd  15642  lmod0vs  15679  islss3  15732  lspsn  15775  lmodindp1  15787  lmodvsinv2  15810  0lmhm  15813  invlmhm  15815  lmhmf1o  15819  pwsdiaglmhm  15830  lspsntrim  15867  lspabs2  15889  lspabs3  15890  lspexch  15898  lpi0  16015  lpi1  16016  ressmplbas2  16215  mplcoe3  16226  mplcoe2  16227  mplmon2  16250  ply1basfvi  16335  coe1subfv  16359  coe1tmmul2  16368  zndvds  16519  znf1o  16521  cygznlem3  16539  ipsubdir  16562  ipsubdi  16563  pjdm2  16627  pjf2  16630  toponcom  16684  tgtopon  16725  indistopon  16754  clsval2  16803  opncldf1  16837  mretopd  16845  toponmre  16846  restopnb  16922  ordtcnv  16947  lecldbas  16965  ordtrestixx  16968  iscncl  17014  cnprest  17033  pnrmopn  17087  ordtt1  17123  2ndcctbss  17197  kgenval  17246  elptr  17284  ptunimpt  17306  ptpjopn  17322  ptcld  17323  hausdiag  17355  qtopeu  17423  pt1hmeo  17513  ptuncnv  17514  ptunhmeo  17515  qtophmeo  17524  ufileu  17630  elfm3  17661  rnelfmlem  17663  fmfnfmlem3  17667  flffval  17700  isfcls  17720  ptcmplem5  17766  prdstmdd  17822  prdstgpd  17823  blfval  17963  setsms  18042  imasf1oxms  18051  stdbdmopn  18080  isngp4  18149  nmrtri  18161  nminvr  18196  lssnlm  18227  cnmet  18297  metds0  18370  metdstri  18371  metdseq0  18374  xrhmeo  18460  icccvx  18464  pcoass  18538  pcorevlem  18540  pcophtb  18543  elpi1i  18560  pi1xfr  18569  pi1xfrcnvlem  18570  lmhmclm  18600  clmmulg  18607  zlmclm  18609  clmzlmvsca  18610  tchcph  18683  cmetss  18756  pmltpclem2  18825  elovolmr  18851  iundisj2  18922  voliunlem1  18923  iunmbl2  18930  ioombl1lem4  18934  uniioombllem3  18956  uniioombllem4  18957  uniioombllem6  18959  dyadmaxlem  18968  volivth  18978  vitalilem3  18981  mbfsub  19033  mbfsup  19035  itg1addlem4  19070  itg1mulc  19075  mbfi1fseqlem6  19091  itgfsum  19197  itgsplitioo  19208  dvaddf  19307  dvexp  19318  dvcnvlem  19339  dvexp3  19341  dveflem  19342  rolle  19353  dvlip  19356  lhop1lem  19376  dvfsumlem1  19389  dvfsumlem3  19391  tdeglem4  19462  tdeglem2  19463  deg1suble  19509  ply1divalg2  19540  facth1  19566  fta1glem1  19567  dvply2g  19681  plydivlem3  19691  fta1lem  19703  quotcan  19705  aaliou3lem7  19745  aaliou3  19747  dvntaylp  19766  ulm2  19780  ulmclm  19782  mtest  19797  mbfulm  19798  pserulm  19814  abelthlem3  19825  abelthlem8  19831  reeff1o  19839  coseq0negpitopi  19887  abssinper  19902  sineq0  19905  cosord  19910  efiarg  19977  logdivlt  19988  logcnlem4  20008  logtayl  20023  dvcxp1  20098  dvcxp2  20099  sqrcn  20106  cxpeq  20113  ang180lem2  20124  ang180lem3  20125  logrec  20133  isosctrlem2  20135  isosctrlem3  20136  angpieqvd  20144  dcubic2  20156  cubic2  20160  dquartlem2  20164  dquart  20165  asinlem3  20183  atans2  20243  rlimcnp  20276  rlimcnp2  20277  amgmlem  20300  ftalem5  20330  dvdsppwf1o  20442  sgmmul  20456  perfect  20486  bcmono  20532  efexple  20536  bposlem1  20539  bposlem9  20547  lgsvalmod  20570  lgsneg  20574  lgsdchrval  20602  lgsquadlem1  20609  lgsquadlem2  20610  chtppilimlem1  20638  rpvmasumlem  20652  dchrisumlema  20653  dchrisumlem2  20655  dchrmusum2  20659  dchrvmasumlem1  20660  dchrvmasum2lem  20661  dchrvmasum2if  20662  dchrvmasumiflem1  20666  dchrisum0fmul  20671  dchrisum0lem2  20683  rplogsum  20692  selberg2lem  20715  logdivbnd  20721  pntrsumo1  20730  selberg3r  20734  selberg4r  20735  selberg34r  20736  pntrlog2bndlem2  20743  pntrlog2bndlem4  20745  qrngdiv  20789  isgrpo  20879  isgrpoi  20881  grpoidinvlem2  20888  grpoinvid2  20914  grpoinvf  20923  isgrpda  20980  subgoinv  20991  exidu1  21009  cmpidelt  21012  ablomul  21038  rngoideu  21067  rngo2  21071  rngolz  21084  rngorz  21085  rngmgmbs4  21100  rngorn1eq  21103  rngosn3  21109  nvmtri2  21254  dipcj  21306  sspg  21320  ssps  21322  sspn  21328  nmlno0lem  21387  cncph  21413  ipasslem2  21426  siii  21447  ubthlem1  21465  ubthlem2  21466  hlipcj  21506  hiidge0  21693  bcseqi  21715  shuni  21895  shunssi  21963  pjhthlem2  21987  shlub  22009  pjop  22022  pjpo  22023  h1de2i  22148  fh1  22213  fh2  22214  chscllem2  22233  chscllem3  22234  pjo  22266  pjcji  22279  hmopre  22519  adjvalval  22533  hmopadj  22535  hmoplin  22538  idhmop  22578  nmlnop0iALT  22591  nmopun  22610  cnvbraval  22706  bracnlnval  22710  kbass3  22714  pjhmopi  22742  hstoh  22828  sto2i  22833  atom1d  22949  atcv0eq  22975  atcv1  22976  ifeqeqx  23050  ballotlemfp1  23066  ballotlemsf1o  23088  ballotlemrinv0  23107  difeq  23144  ifbieq12d2  23165  fimacnvinrn  23214  fmptcof2  23244  xlt2addrd  23268  xrge0pluscn  23337  iundisj2fi  23379  iundisj2f  23381  logbrec  23422  esumval  23440  esumel  23441  esumc  23445  esumpfinvallem  23457  esumpcvgval  23461  esumpmono  23462  esumcocn  23463  unisg  23519  indf1ofs  23624  probmeasb  23648  zetacvg  23704  subfacp1lem5  23730  subfacval2  23733  subfacval3  23735  conpcon  23781  sconpi1  23785  umgraex  23890  eupath2  23919  relexpcnv  24044  relexpadd  24050  rtrclreclem.trans  24058  dfrtrcl2  24060  fprodcvg  24153  prodmolem3  24156  tfisg  24275  wfr3g  24326  tfr3ALT  24350  frr3g  24351  nofnbday  24377  sltres  24389  nodense  24414  colinearalglem2  24607  ax5seglem9  24637  axpaschlem  24640  axpasch  24641  axcontlem7  24670  fvtransport  24727  transportprops  24729  btwnconn1lem12  24793  midofsegid  24799  outsideofeq  24825  lineunray  24842  bpolysum  24860  fsumcube  24867  rankeq1o  24873  onsuctopon  24945  supaddc  24995  itg2addnclem  25003  areacirclem2  25028  areacirclem5  25032  moec  25150  domrngref  25163  domfldref  25164  cnvref2  25169  mapex2  25243  repfuntw  25263  cbicp  25269  prl2  25272  valcurfn1  25307  sege  25355  mxlmnl2  25373  defse3  25375  supwval  25387  dffprod  25422  fprodp1  25426  iscom  25436  reacomsmgrp1  25446  reacomsmgrp2  25447  reacomsmgrp4  25449  resgcom  25454  trran2  25496  ltrran2  25506  ltrooo  25507  ltrinvlem  25509  rltrran  25517  multinv  25525  multinvb  25526  addvecass  25568  dblsubvec  25577  mvecrtol2  25580  mulveczer  25582  mulinvsca  25583  svli2  25587  svs2  25590  svs3  25591  inttop4  25620  sallnei  25632  intopcoaconlem3b  25641  intopcoaconlem3  25642  mslb1  25710  2wsms  25711  trran  25717  supnuf  25732  addcanrg  25770  negveud  25771  negveudr  25772  mulmulvec  25790  distsava  25792  dcsda  25836  1ded  25841  rcmob  25852  dmrngcmp  25854  1cat  25862  morcat  25883  cmpassoh  25904  homgrf  25905  imonclem  25916  cmpmon  25918  icmpmon  25919  isfuna  25937  idfisf  25944  idsubidsup  25960  idsubfun  25961  vtarl  25990  rocatval  26062  cmp2morpcats  26064  cmpmorass  26069  morexcmp2  26071  cmpidmor3  26073  cmppar3  26077  segline  26244  bhp3  26280  nn0prpwlem  26341  opnbnd  26346  cldbnd  26347  refssfne  26397  fnejoin2  26421  sdclem2  26555  trirn  26566  stiooOLD  26574  isbnd2  26610  ghomdiv  26677  rngogrphom  26705  0rngo  26755  prnc  26795  isdmn3  26802  prtlem11  26837  elrfi  26872  elrfirn  26873  mapfzcons  26896  mzprename  26930  eldioph2b  26945  lzenom  26952  diophin  26955  eq0rabdioph  26959  rexrabdioph  26978  rexzrexnn0  26988  fphpdo  27003  irrapxlem2  27011  irrapxlem3  27012  irrapxlem5  27014  pellexlem2  27018  pellexlem6  27022  pell1234qrdich  27049  pell14qrdich  27057  pell1qrge1  27058  pell1qrgaplem  27061  pellfund14gap  27075  qirropth  27096  rmxyelqirr  27098  rmxycomplete  27105  rmxy1  27110  rmym1  27123  rmxluc  27124  rmxdbl  27127  acongtr  27168  jm2.18  27184  jm2.22  27191  jm2.23  27192  jm2.25  27195  jm2.26lem3  27197  jm2.27a  27201  jm2.27c  27203  fnwe2lem3  27252  kelac1  27264  pwssplit4  27294  filnm  27295  pwslnmlem2  27298  frlmpws  27321  frlmlss  27322  frlmlbs  27352  frlmup3  27355  ellspd  27357  unxpwdom3  27359  imasgim  27367  isnumbasgrplem3  27373  lsslindf  27403  islindf4  27411  islindf5  27412  hbt  27437  mpaaeu  27458  rngunsnply  27481  en2eleq  27484  pmtrfrn  27503  psgnunilem1  27519  hashgcdlem  27619  proot1ex  27623  ofdivrec  27646  iotaexeu  27721  iotasbc  27722  pm14.24  27735  sbiota1  27737  cncmpmax  27806  refsum2cnlem1  27811  cncfmptss  27820  expcnfg  27829  clim1fr1  27830  isumneg  27831  climexp  27834  climneg  27839  climdivf  27841  itgsin0pilem1  27847  ibliccsinexp  27848  itgsinexplem1  27851  itgsinexp  27852  stoweidlem1  27853  stoweidlem2  27854  stoweidlem3  27855  stoweidlem11  27863  stoweidlem13  27865  stoweidlem19  27871  stoweidlem21  27873  stoweidlem24  27876  stoweidlem26  27878  stoweidlem29  27881  stoweidlem40  27892  stoweidlem42  27894  stoweidlem55  27907  stoweidlem59  27911  stoweidlem62  27914  wallispilem4  27920  wallispilem5  27921  wallispi  27922  wallispi2lem1  27923  wallispi2lem2  27924  stirlinglem1  27926  stirlinglem3  27928  stirlinglem4  27929  stirlinglem5  27930  stirlinglem6  27931  stirlinglem7  27932  stirlinglem8  27933  stirlinglem10  27935  stirlinglem11  27936  stirlinglem12  27937  stirlinglem15  27940  sigaras  27948  sigarms  27949  sigarperm  27953  sharhght  27958  afvelrn  28136  afvres  28140  dmfcoafv  28143  afvco2  28144  mpt2xopoveqd  28203  injresinj  28215  elprchashprn2  28216  s4f1o  28225  nbgraop  28274  uvtxnbgra  28306  redwlk  28364  fargshiftlem  28379  fargshiftfo  28383  fargshiftfva  28384  eupatrl  28385  onetansqsecsq  28485  csbsngVD  28985  bnj1241  29156  bnj548  29245  lsatel  29817  lsatfixedN  29821  lsat0cv  29845  ldualgrplem  29957  lduallmodlem  29964  lkrpssN  29975  lkreqN  29982  omlfh1N  30070  atcvreq0  30126  glbconN  30188  2atjm  30256  hlatexch3N  30291  lplnexllnN  30375  2llnjaN  30377  2lplnja  30430  dalem56  30539  2llnma1b  30597  atmod1i1  30668  atmod1i2  30670  llnmod1i2  30671  dalawlem11  30692  pclfinN  30711  osumclN  30778  4atexlemswapqr  30874  4atexlemunv  30877  cdleme15a  31085  cdleme16  31096  cdleme22cN  31153  cdleme22d  31154  cdleme43dN  31303  cdlemeg46sfg  31331  cdlemeg46fjgN  31332  cdlemg1a  31381  cdlemeiota  31396  cdlemg3a  31408  cdlemg12e  31458  cdlemg18a  31489  trlcone  31539  tgrpgrplem  31560  tgrpabl  31562  cdlemk4  31645  cdlemksv2  31658  cdlemkuv2  31678  cdlemk19  31680  cdlemk22  31704  cdlemk53a  31766  erngdvlem1  31799  erngdvlem2N  31800  erngdvlem3  31801  erngdvlem4  31802  erngdvlem1-rN  31807  erngdvlem2-rN  31808  erngdvlem3-rN  31809  erngdvlem4-rN  31810  dvalveclem  31837  dialss  31858  dia2dimlem2  31877  dia2dimlem3  31878  dvhgrp  31919  dvhlveclem  31920  cdlemm10N  31930  doca2N  31938  diblss  31982  dicvaddcl  32002  dicvscacl  32003  dicn0  32004  diclss  32005  cdlemn11a  32019  dihjust  32029  dihopelvalcpre  32060  dihmeetlem5  32120  dochlkr  32197  dihsmatrn  32248  dvh4dimat  32250  mapdval4N  32444  mapdcv  32472  mapdpglem15  32498  baerlem5bmN  32529  baerlem5abmN  32530  mapdh8aa  32588  hdmapval3lemN  32652  hdmap10lem  32654  hdmaprnlem10N  32674  hdmap14lem2a  32682  hdmap14lem2N  32684  hdmap14lem3  32685  hdmap14lem6  32688  hgmapvs  32706  hlhilocv  32772  hlhillcs  32773
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator