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

Theorem eqcomd 2443
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 2440 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2sylib 190 1  |-  ( ph  ->  B  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653
This theorem is referenced by:  eqtr2d  2471  eqtr3d  2472  eqtr4d  2473  syl5req  2483  syl6req  2487  sylan9req  2491  eqeltrrd  2513  eleqtrrd  2515  syl5eleqr  2525  syl6eqelr  2527  eqnetrrd  2623  neeqtrrd  2627  dedhb  3106  eqsstr3d  3385  sseqtr4d  3387  syl6eqssr  3401  dfrab3ss  3621  uneqdifeq  3718  ifbi  3758  ifbothda  3771  dedth  3782  elimhyp  3789  elimhyp2v  3790  elimhyp3v  3791  elimhyp4v  3792  elimdhyp  3794  keephyp2v  3796  keephyp3v  3797  disjsn2  3871  diftpsn3  3939  unimax  4051  iununi  4178  sndisj  4207  disjprg  4211  eqbrtrrd  4237  breqtrrd  4241  syl5breqr  4251  syl6eqbrr  4253  class2seteq  4371  opth1  4437  euotd  4460  opelopabsb  4468  ordsuc  4797  tfisi  4841  0nelxp  4909  opeliunxp  4932  sosn  4950  somincom  5274  iotaex  5438  iota4  5439  fun2ssres  5497  funimass1  5529  funssfv  5749  fnimapr  5790  fvun  5796  fmptco  5904  fnpr  5953  fnprOLD  5954  foeqcnvco  6030  f1eqcocnv  6031  f1oiso2  6075  f1opw2  6301  sbcopeq1a  6402  csbopeq1a  6403  eloprabi  6416  f2ndf  6455  mpt2xopoveqd  6475  riotass2  6580  riotass  6581  f1ocnvfv3  6588  riotasvdOLD  6596  riotasv3d  6601  riotasv3dOLD  6602  smoiso  6627  seqomlem4  6713  omopth2  6830  eqer  6941  uniqs  6967  mapsncnv  7063  ixpiin  7091  undifixp  7101  mapsnf1o  7106  mapunen  7279  ssenen  7284  pssnn  7330  en1eqsn  7341  findcard2  7351  unblem2  7363  domunfican  7382  fofinf1o  7390  f1opwfi  7413  inelfi  7426  marypha1lem  7441  ixpiunwdom  7562  infdifsn  7614  oemapwe  7653  rankpwi  7752  rankuni  7792  cardsucinf  7876  en2eqpr  7896  iunmapdisj  7909  infpwfien  7948  alephfp  7994  infmap2  8103  ackbij1lem16  8120  ackbij2  8128  cfsuc  8142  cfss  8150  enfin2i  8206  fin23lem22  8212  fin1a2lem6  8290  fin1a2lem11  8295  axcc2lem  8321  axcclem  8342  iundom2g  8420  ficard  8445  konigthlem  8448  fpwwe2lem8  8517  fpwwe2lem13  8522  fpwwe2  8523  canth4  8527  pwfseqlem4  8542  winalim2  8576  addassnq  8840  mulassnq  8841  distrnq  8843  ltsonq  8851  lterpq  8852  1idpr  8911  recexsrlem  8983  le2tri3i  9208  mul02lem2  9248  subdi  9472  infm3lem  9971  supmul1  9978  cru  9997  nn0ge0  10252  elz2  10303  zaddcl  10322  zindd  10376  xmulge0  10868  xadddi2  10881  prunioo  11030  fseq1p1m1  11127  fzrevral  11136  injresinj  11205  fllelt  11211  flval2  11226  modcyc  11281  uzrdgsuci  11305  fzen2  11313  axdc4uzlem  11326  seqf1olem1  11367  seqf1olem2  11368  sersub  11371  expgt1  11423  leexp2r  11442  sq01  11506  modexp  11519  bcm1k  11611  bcn2m1  11620  hashunx  11665  hashprg  11671  elprchashprn2  11672  hashssdif  11682  hashmap  11703  hashbc  11707  hashf1lem1  11709  hashf1lem2  11710  swrds1  11792  s4f1o  11870  shftlem  11888  shftfval  11890  replim  11926  cjexp  11960  sqrlem2  12054  sqrlem7  12059  resqrthlem  12065  abssq  12116  recan  12145  sqrthlem  12171  climmpt  12370  fsumcvg  12511  fsumcom2  12563  fsumconst  12578  fsumless  12580  cvgcmpce  12602  abscvgcvg  12603  incexclem  12621  isumsplit  12625  climcndslem1  12634  arisum  12644  geoserg  12650  geo2sum  12655  mertenslem1  12666  mertenslem2  12667  efcj  12699  efsub  12706  eflegeo  12727  sinneg  12752  cosneg  12753  sin01bnd  12791  cos01bnd  12792  divalgmod  12931  bitsinv1  12959  bitsf1ocnv  12961  gcdneg  13031  bezoutlem1  13043  bezoutlem3  13045  dvdssq  13065  isprm2lem  13091  isprm5  13117  divnumden  13145  zgcdsq  13150  phibnd  13165  pythagtriplem19  13212  iserodd  13214  pcprendvds2  13220  pczpre  13226  prmreclem1  13289  prmreclem4  13292  4sqlem4  13325  prmlem0  13433  strfvi  13512  topnval  13667  prdssca  13684  imasbas  13743  imasvscafn  13767  mrieqvlemd  13859  mrissmrcd  13870  catideu  13905  subcid  14049  funcres  14098  fucbas  14162  fuchom  14163  resssetc  14252  resscatc  14265  catcisolem  14266  xpcbas  14280  yonffthlem  14384  pospo  14435  lubprop  14442  glbprop  14447  acsinfdimd  14613  ismgmid2  14718  mndfo  14725  prds0g  14734  0mhm  14763  pwspjmhm  14772  gsumvallem1  14776  gsumval2a  14787  gsumccat  14792  gsumwmhm  14795  gsumwspan  14796  frmdval  14801  grpidd2  14847  grpinvid2  14859  grpnpcan  14885  grpsubsub4  14886  mulgfvi  14899  divsgrp2  14941  divs0  15003  ghmid  15017  ghminv  15018  gicsubgen  15070  gafo  15078  orbsta  15095  symgid  15109  cntrval  15123  oppgmnd  15155  oppginv  15160  mndodcong  15185  odval2  15194  odeq1  15201  odf1o1  15211  odf1o2  15212  odhash3  15215  gexdvds  15223  sylow2alem2  15257  lsmelvalm  15290  lsmmod2  15313  pj1lid  15338  pj1rid  15339  efginvrel2  15364  efgredleme  15380  efgredlemc  15382  efgredlemb  15383  efgrelexlemb  15387  frgp0  15397  lt6abl  15509  gsumzaddlem  15531  gsumcom2  15554  dprdfcntz  15578  dprdf1o  15595  dprd2da  15605  dpjrid  15625  pgpfac1lem3a  15639  pgpfaclem1  15644  ablfaclem3  15650  mgpress  15664  rnglz  15705  rngrz  15706  rngnegl  15708  rngnegr  15709  prdsmgp  15721  imasrng  15730  divsrng2  15731  opprrng  15741  crngunit  15772  issrngd  15954  lmod0vs  15988  islss3  16040  lspsn  16083  lmodindp1  16095  lmodvsinv2  16118  0lmhm  16121  invlmhm  16123  lmhmf1o  16127  pwsdiaglmhm  16138  lspsntrim  16175  lspabs2  16197  lspabs3  16198  lspexch  16206  lpi0  16323  lpi1  16324  ressmplbas2  16523  mplcoe3  16534  mplcoe2  16535  mplmon2  16558  ply1basfvi  16640  coe1subfv  16664  coe1tmmul2  16673  zndvds  16835  znf1o  16837  cygznlem3  16855  ipsubdir  16878  ipsubdi  16879  pjdm2  16943  pjf2  16946  toponcom  17000  tgtopon  17041  indistopon  17070  clsval2  17119  opncldf1  17153  mretopd  17161  toponmre  17162  neiptopuni  17199  neiptopreu  17202  restopnb  17244  ordtcnv  17270  lecldbas  17288  ordtrestixx  17291  iscncl  17338  cnprest  17358  pnrmopn  17412  ordtt1  17448  2ndcctbss  17523  kgenval  17572  elptr  17610  ptunimpt  17632  ptpjopn  17649  ptcld  17650  hausdiag  17682  qtopeu  17753  pt1hmeo  17843  ptuncnv  17844  ptunhmeo  17845  qtophmeo  17854  ufileu  17956  elfm3  17987  rnelfmlem  17989  fmfnfmlem3  17993  flffval  18026  isfcls  18046  ptcmplem5  18092  prdstmdd  18158  prdstgpd  18159  utopbas  18270  restutopopn  18273  ustuqtop1  18276  ustuqtop3  18278  ustuqtop5  18280  blfvalps  18418  setsms  18515  imasf1oxms  18524  stdbdmopn  18553  isngp4  18663  nmrtri  18675  nminvr  18710  lssnlm  18741  cnmet  18811  metds0  18885  metdstri  18886  metdseq0  18889  xrhmeo  18976  icccvx  18980  pcoass  19054  pcorevlem  19056  pcophtb  19059  elpi1i  19076  pi1xfr  19085  pi1xfrcnvlem  19086  lmhmclm  19116  clmmulg  19123  zlmclm  19125  clmzlmvsca  19126  tchcph  19199  cmetss  19272  pmltpclem2  19351  elovolmr  19377  iundisj2  19448  voliunlem1  19449  iunmbl2  19456  ioombl1lem4  19460  uniioombllem3  19482  uniioombllem4  19483  uniioombllem6  19485  dyadmaxlem  19494  volivth  19504  vitalilem3  19507  mbfsub  19557  mbfsup  19559  itg1addlem4  19594  itg1mulc  19599  mbfi1fseqlem6  19615  itgfsum  19721  itgsplitioo  19732  dvaddf  19833  dvexp  19844  dvcnvlem  19865  dvexp3  19867  dveflem  19868  rolle  19879  dvlip  19882  lhop1lem  19902  dvfsumlem1  19915  dvfsumlem3  19917  tdeglem4  19988  tdeglem2  19989  deg1suble  20035  ply1divalg2  20066  facth1  20092  fta1glem1  20093  dvply2g  20207  plydivlem3  20217  fta1lem  20229  quotcan  20231  aaliou3lem7  20271  aaliou3  20273  dvntaylp  20292  ulm2  20306  ulmclm  20308  ulmuni  20313  mtest  20325  mbfulm  20327  pserulm  20343  abelthlem3  20354  abelthlem8  20360  reeff1o  20368  coseq0negpitopi  20416  abssinper  20431  sineq0  20434  cosord  20439  efiarg  20507  abslogle  20518  logdivlt  20521  logcnlem4  20541  logtayl  20556  dvcxp1  20631  dvcxp2  20632  sqrcn  20639  cxpeq  20646  ang180lem2  20657  ang180lem3  20658  logrec  20666  isosctrlem2  20668  isosctrlem3  20669  angpieqvd  20677  dcubic2  20689  cubic2  20693  dquartlem2  20697  dquart  20698  asinlem3  20716  atans2  20776  rlimcnp  20809  rlimcnp2  20810  amgmlem  20833  ftalem5  20864  dvdsppwf1o  20976  sgmmul  20990  perfect  21020  bcmono  21066  efexple  21070  bposlem1  21073  bposlem9  21081  lgsvalmod  21104  lgsneg  21108  lgsdchrval  21136  lgsquadlem2  21144  chtppilimlem1  21172  rpvmasumlem  21186  dchrisumlema  21187  dchrisumlem2  21189  dchrmusum2  21193  dchrvmasumlem1  21194  dchrvmasum2lem  21195  dchrvmasum2if  21196  dchrvmasumiflem1  21200  dchrisum0fmul  21205  dchrisum0lem2  21217  rplogsum  21226  selberg2lem  21249  logdivbnd  21255  pntrsumo1  21264  selberg3r  21268  selberg4r  21269  selberg34r  21270  pntrlog2bndlem2  21277  pntrlog2bndlem4  21279  qrngdiv  21323  umgraex  21363  nbgraop  21441  cusgrasizeinds  21490  cusgrasize2inds  21491  cusgrafilem2  21494  uvtxnbgra  21507  0wlkon  21552  redwlk  21611  fargshiftlem  21626  fargshiftfo  21630  fargshiftfva  21631  dfconngra1  21663  eupatrl  21695  eupath2  21707  isgrpo  21789  isgrpoi  21791  grpoidinvlem2  21798  grpoinvid2  21824  grpoinvf  21833  isgrpda  21890  subgoinv  21901  exidu1  21919  cmpidelt  21922  ablomul  21948  rngoideu  21977  rngo2  21981  rngolz  21994  rngorz  21995  rngmgmbs4  22010  rngorn1eq  22013  rngosn3  22019  nvmtri2  22166  dipcj  22218  sspg  22232  ssps  22234  sspn  22240  nmlno0lem  22299  cncph  22325  ipasslem2  22338  siii  22359  ubthlem1  22377  ubthlem2  22378  hlipcj  22418  hiidge0  22605  bcseqi  22627  shuni  22807  shunssi  22875  pjhthlem2  22899  shlub  22921  pjop  22934  pjpo  22935  h1de2i  23060  fh1  23125  fh2  23126  chscllem2  23145  chscllem3  23146  pjo  23178  pjcji  23191  hmopre  23431  adjvalval  23445  hmopadj  23447  hmoplin  23450  idhmop  23490  nmlnop0iALT  23503  nmopun  23522  cnvbraval  23618  bracnlnval  23622  kbass3  23626  pjhmopi  23654  hstoh  23740  sto2i  23745  atom1d  23861  atcv0eq  23887  atcv1  23888  ifeqeqx  24006  ifbieq12d2  24007  iundisj2f  24035  imadifxp  24043  ofresid  24060  fmptcof2  24081  xlt2addrd  24129  iundisj2fi  24158  ofldchr  24249  redvr  24282  xrge0pluscn  24331  qqhval2lem  24370  qqhval2  24371  rrhcn  24385  logbrec  24410  indf1ofs  24428  esumel  24447  esumc  24451  gsumesum  24456  esumfsup  24465  esumfsupre  24466  esumpfinvallem  24469  esumpcvgval  24473  esumpmono  24474  esumcocn  24475  unisg  24531  voliune  24590  volfiniune  24591  probmeasb  24693  ballotlemfp1  24754  ballotlemsf1o  24776  ballotlemrinv0  24795  zetacvg  24804  lgamgulmlem2  24819  lgamgulmlem3  24820  lgamcvg2  24844  gamcvg2lem  24848  subfacp1lem5  24875  subfacval2  24878  subfacval3  24880  conpcon  24927  sconpi1  24931  relexpcnv  25138  relexpadd  25143  rtrclreclem.trans  25151  dfrtrcl2  25153  clim2div  25222  fprodcvg  25261  fprodss  25279  fprodser  25280  fprodconst  25307  fprodcom2  25313  iprodfac  25371  tfisg  25484  wfr3g  25542  tfr3ALT  25565  frr3g  25586  nofnbday  25612  sltres  25624  nodense  25649  colinearalglem2  25851  ax5seglem9  25881  axpaschlem  25884  axpasch  25885  axcontlem7  25914  fvtransport  25971  transportprops  25973  btwnconn1lem12  26037  midofsegid  26043  outsideofeq  26069  lineunray  26086  bpolysum  26104  fsumcube  26111  rankeq1o  26117  onsuctopon  26189  supaddc  26245  heicant  26253  mblfinlem3  26257  mblfinlem4  26258  ismblfin  26259  itg2addnclem  26270  itg2addnc  26273  ftc1anclem5  26298  ftc1anclem7  26300  areacirclem1  26306  areacirclem4  26309  nn0prpwlem  26339  opnbnd  26342  cldbnd  26343  refssfne  26388  fnejoin2  26412  sdclem2  26460  trirn  26471  isbnd2  26506  ghomdiv  26573  rngogrphom  26601  0rngo  26651  prnc  26691  isdmn3  26698  prtlem11  26729  elrfi  26762  elrfirn  26763  mapfzcons  26786  mzprename  26820  eldioph2b  26835  lzenom  26842  diophin  26845  eq0rabdioph  26849  rexrabdioph  26868  rexzrexnn0  26878  fphpdo  26892  irrapxlem2  26900  irrapxlem3  26901  irrapxlem5  26903  pellexlem2  26907  pellexlem6  26911  pell1234qrdich  26938  pell14qrdich  26946  pell1qrge1  26947  pell1qrgaplem  26950  pellfund14gap  26964  qirropth  26985  rmxyelqirr  26987  rmxycomplete  26994  rmxy1  26999  rmym1  27012  rmxluc  27013  rmxdbl  27016  acongtr  27057  jm2.18  27073  jm2.22  27080  jm2.23  27081  jm2.25  27084  jm2.26lem3  27086  jm2.27a  27090  jm2.27c  27092  fnwe2lem3  27141  kelac1  27152  pwssplit4  27182  filnm  27183  pwslnmlem2  27186  frlmpws  27209  frlmlss  27210  frlmlbs  27240  frlmup3  27243  ellspd  27245  unxpwdom3  27247  imasgim  27255  isnumbasgrplem3  27261  lsslindf  27291  islindf4  27299  islindf5  27300  hbt  27325  mpaaeu  27346  rngunsnply  27369  en2eleq  27372  pmtrfrn  27391  psgnunilem1  27407  hashgcdlem  27507  proot1ex  27511  ofdivrec  27534  iotaexeu  27609  iotasbc  27610  pm14.24  27623  sbiota1  27625  cncmpmax  27693  refsum2cnlem1  27698  expcnfg  27716  clim1fr1  27717  isumneg  27718  climneg  27726  climdivf  27728  itgsin0pilem1  27734  ibliccsinexp  27735  itgsinexplem1  27738  itgsinexp  27739  stoweidlem2  27741  stoweidlem3  27742  stoweidlem13  27752  stoweidlem19  27758  stoweidlem21  27760  stoweidlem24  27763  stoweidlem26  27765  stoweidlem29  27768  stoweidlem40  27779  stoweidlem42  27781  stoweidlem62  27801  wallispilem4  27807  wallispi  27809  wallispi2lem1  27810  wallispi2lem2  27811  stirlinglem1  27813  stirlinglem3  27815  stirlinglem4  27816  stirlinglem5  27817  stirlinglem6  27818  stirlinglem7  27819  stirlinglem8  27820  stirlinglem10  27822  stirlinglem12  27824  stirlinglem15  27827  sigaras  27835  sigarms  27836  sigarperm  27840  sharhght  27845  afvelrn  28022  afvres  28026  dmfcoafv  28029  afvco2  28030  2if2  28067  resisresindm  28089  imarnf1pr  28102  elovmpt3rab  28108  fzosplitsnm1  28154  flpmodeq  28173  modifeq2int  28184  ccatsymb  28211  wrdlenccats1lenm1  28212  elovmpt2wrd  28213  elovmptnn0wrd  28214  ccats1swrdid  28225  swrd0fv  28226  swrd0swrd  28231  swrdswrd  28233  swrdswrd0  28235  swrdccatfn  28238  swrdccatin12lem3b  28243  swrdccatin12lem3  28246  swrdccat3blem  28252  swrdccat3b  28253  modprm1div  28258  reumodprminv  28261  cshwidx  28276  cshwidxmod  28277  2cshw2lem3  28288  2cshwmod  28291  lstccats1fst  28297  cshwleneq  28302  3cshw  28303  cshweqdif2  28304  cshwssizelem4a  28317  wlklenfislenpm1  28337  usgra2adedgwlk  28354  wlkiswwlk1  28372  wlklniswwlkn2  28382  usg2spthonot  28420  usg2spthonot0  28421  frgraunss  28459  frgrancvvdeqlem4  28496  frg2woteq  28523  onetansqsecsq  28578  csbsngVD  29079  isosctrlem1ALT  29120  sineq0ALT  29123  bnj1241  29253  bnj548  29342  lsatel  29877  lsatfixedN  29881  lsat0cv  29905  ldualgrplem  30017  lduallmodlem  30024  lkrpssN  30035  lkreqN  30042  omlfh1N  30130  atcvreq0  30186  glbconN  30248  2atjm  30316  hlatexch3N  30351  lplnexllnN  30435  2llnjaN  30437  2lplnja  30490  dalem56  30599  2llnma1b  30657  atmod1i1  30728  atmod1i2  30730  llnmod1i2  30731  dalawlem11  30752  pclfinN  30771  osumclN  30838  4atexlemswapqr  30934  4atexlemunv  30937  cdleme15a  31145  cdleme16  31156  cdleme22cN  31213  cdleme22d  31214  cdleme43dN  31363  cdlemeg46sfg  31391  cdlemeg46fjgN  31392  cdlemg1a  31441  cdlemeiota  31456  cdlemg3a  31468  cdlemg12e  31518  cdlemg18a  31549  trlcone  31599  tgrpgrplem  31620  tgrpabl  31622  cdlemk4  31705  cdlemksv2  31718  cdlemkuv2  31738  cdlemk19  31740  cdlemk22  31764  cdlemk53a  31826  erngdvlem1  31859  erngdvlem2N  31860  erngdvlem3  31861  erngdvlem4  31862  erngdvlem1-rN  31867  erngdvlem2-rN  31868  erngdvlem3-rN  31869  erngdvlem4-rN  31870  dvalveclem  31897  dialss  31918  dia2dimlem2  31937  dia2dimlem3  31938  dvhgrp  31979  dvhlveclem  31980  cdlemm10N  31990  doca2N  31998  diblss  32042  dicvaddcl  32062  dicvscacl  32063  dicn0  32064  diclss  32065  cdlemn11a  32079  dihjust  32089  dihopelvalcpre  32120  dihmeetlem5  32180  dochlkr  32257  dihsmatrn  32308  dvh4dimat  32310  mapdval4N  32504  mapdcv  32532  mapdpglem15  32558  baerlem5bmN  32589  baerlem5abmN  32590  mapdh8aa  32648  hdmapval3lemN  32712  hdmap10lem  32714  hdmaprnlem10N  32734  hdmap14lem2a  32742  hdmap14lem2N  32744  hdmap14lem3  32745  hdmap14lem6  32748  hgmapvs  32766  hlhilocv  32832  hlhillcs  32833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-cleq 2431
  Copyright terms: Public domain W3C validator