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

Theorem eqcomd 2440
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 2437 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2sylib 189 1  |-  ( ph  ->  B  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  eqtr2d  2468  eqtr3d  2469  eqtr4d  2470  syl5req  2480  syl6req  2484  sylan9req  2488  eqeltrrd  2510  eleqtrrd  2512  syl5eleqr  2522  syl6eqelr  2524  eqnetrrd  2618  neeqtrrd  2622  dedhb  3096  eqsstr3d  3375  sseqtr4d  3377  syl6eqssr  3391  dfrab3ss  3611  uneqdifeq  3708  ifbi  3748  ifbothda  3761  dedth  3772  elimhyp  3779  elimhyp2v  3780  elimhyp3v  3781  elimhyp4v  3782  elimdhyp  3784  keephyp2v  3786  keephyp3v  3787  disjsn2  3861  diftpsn3  3929  unimax  4041  iununi  4167  sndisj  4196  disjprg  4200  eqbrtrrd  4226  breqtrrd  4230  syl5breqr  4240  syl6eqbrr  4242  class2seteq  4360  opth1  4426  euotd  4449  opelopabsb  4457  ordsuc  4786  tfisi  4830  0nelxp  4898  opeliunxp  4921  sosn  4939  somincom  5263  iotaex  5427  iota4  5428  fun2ssres  5486  funimass1  5518  funssfv  5738  fnimapr  5779  fvun  5785  fmptco  5893  fnpr  5942  fnprOLD  5943  foeqcnvco  6019  f1eqcocnv  6020  f1oiso2  6064  f1opw2  6290  sbcopeq1a  6391  csbopeq1a  6392  eloprabi  6405  f2ndf  6444  mpt2xopoveqd  6464  riotass2  6569  riotass  6570  f1ocnvfv3  6577  riotasvdOLD  6585  riotasv3d  6590  riotasv3dOLD  6591  smoiso  6616  seqomlem4  6702  omopth2  6819  eqer  6930  uniqs  6956  mapsncnv  7052  ixpiin  7080  undifixp  7090  mapsnf1o  7095  mapunen  7268  ssenen  7273  pssnn  7319  en1eqsn  7330  findcard2  7340  unblem2  7352  domunfican  7371  fofinf1o  7379  f1opwfi  7402  inelfi  7415  marypha1lem  7430  ixpiunwdom  7551  infdifsn  7603  oemapwe  7642  rankpwi  7741  rankuni  7781  cardsucinf  7863  en2eqpr  7883  iunmapdisj  7896  infpwfien  7935  alephfp  7981  infmap2  8090  ackbij1lem16  8107  ackbij2  8115  cfsuc  8129  cfss  8137  enfin2i  8193  fin23lem22  8199  fin1a2lem6  8277  fin1a2lem11  8282  axcc2lem  8308  axcclem  8329  iundom2g  8407  ficard  8432  konigthlem  8435  fpwwe2lem8  8504  fpwwe2lem13  8509  fpwwe2  8510  canth4  8514  pwfseqlem4  8529  winalim2  8563  addassnq  8827  mulassnq  8828  distrnq  8830  ltsonq  8838  lterpq  8839  1idpr  8898  recexsrlem  8970  le2tri3i  9195  mul02lem2  9235  subdi  9459  infm3lem  9958  supmul1  9965  cru  9984  nn0ge0  10239  elz2  10290  zaddcl  10309  zindd  10363  xmulge0  10855  xadddi2  10868  prunioo  11017  fseq1p1m1  11114  fzrevral  11123  injresinj  11192  fllelt  11198  flval2  11213  modcyc  11268  uzrdgsuci  11292  fzen2  11300  axdc4uzlem  11313  seqf1olem1  11354  seqf1olem2  11355  sersub  11358  expgt1  11410  leexp2r  11429  sq01  11493  modexp  11506  bcm1k  11598  bcn2m1  11607  hashunx  11652  hashprg  11658  elprchashprn2  11659  hashssdif  11669  hashmap  11690  hashbc  11694  hashf1lem1  11696  hashf1lem2  11697  swrds1  11779  s4f1o  11857  shftlem  11875  shftfval  11877  replim  11913  cjexp  11947  sqrlem2  12041  sqrlem7  12046  resqrthlem  12052  abssq  12103  recan  12132  sqrthlem  12158  climmpt  12357  fsumcvg  12498  fsumcom2  12550  fsumconst  12565  fsumless  12567  cvgcmpce  12589  abscvgcvg  12590  incexclem  12608  isumsplit  12612  climcndslem1  12621  arisum  12631  geoserg  12637  geo2sum  12642  mertenslem1  12653  mertenslem2  12654  efcj  12686  efsub  12693  eflegeo  12714  sinneg  12739  cosneg  12740  sin01bnd  12778  cos01bnd  12779  divalgmod  12918  bitsinv1  12946  bitsf1ocnv  12948  gcdneg  13018  bezoutlem1  13030  bezoutlem3  13032  dvdssq  13052  isprm2lem  13078  isprm5  13104  divnumden  13132  zgcdsq  13137  phibnd  13152  pythagtriplem19  13199  iserodd  13201  pcprendvds2  13207  pczpre  13213  prmreclem1  13276  prmreclem4  13279  4sqlem4  13312  prmlem0  13420  strfvi  13499  topnval  13654  prdssca  13671  imasbas  13730  imasvscafn  13754  mrieqvlemd  13846  mrissmrcd  13857  catideu  13892  subcid  14036  funcres  14085  fucbas  14149  fuchom  14150  resssetc  14239  resscatc  14252  catcisolem  14253  xpcbas  14267  yonffthlem  14371  pospo  14422  lubprop  14429  glbprop  14434  acsinfdimd  14600  ismgmid2  14705  mndfo  14712  prds0g  14721  0mhm  14750  pwspjmhm  14759  gsumvallem1  14763  gsumval2a  14774  gsumccat  14779  gsumwmhm  14782  gsumwspan  14783  frmdval  14788  grpidd2  14834  grpinvid2  14846  grpnpcan  14872  grpsubsub4  14873  mulgfvi  14886  divsgrp2  14928  divs0  14990  ghmid  15004  ghminv  15005  gicsubgen  15057  gafo  15065  orbsta  15082  symgid  15096  cntrval  15110  oppgmnd  15142  oppginv  15147  mndodcong  15172  odval2  15181  odeq1  15188  odf1o1  15198  odf1o2  15199  odhash3  15202  gexdvds  15210  sylow2alem2  15244  lsmelvalm  15277  lsmmod2  15300  pj1lid  15325  pj1rid  15326  efginvrel2  15351  efgredleme  15367  efgredlemc  15369  efgredlemb  15370  efgrelexlemb  15374  frgp0  15384  lt6abl  15496  gsumzaddlem  15518  gsumcom2  15541  dprdfcntz  15565  dprdf1o  15582  dprd2da  15592  dpjrid  15612  pgpfac1lem3a  15626  pgpfaclem1  15631  ablfaclem3  15637  mgpress  15651  rnglz  15692  rngrz  15693  rngnegl  15695  rngnegr  15696  prdsmgp  15708  imasrng  15717  divsrng2  15718  opprrng  15728  crngunit  15759  issrngd  15941  lmod0vs  15975  islss3  16027  lspsn  16070  lmodindp1  16082  lmodvsinv2  16105  0lmhm  16108  invlmhm  16110  lmhmf1o  16114  pwsdiaglmhm  16125  lspsntrim  16162  lspabs2  16184  lspabs3  16185  lspexch  16193  lpi0  16310  lpi1  16311  ressmplbas2  16510  mplcoe3  16521  mplcoe2  16522  mplmon2  16545  ply1basfvi  16627  coe1subfv  16651  coe1tmmul2  16660  zndvds  16822  znf1o  16824  cygznlem3  16842  ipsubdir  16865  ipsubdi  16866  pjdm2  16930  pjf2  16933  toponcom  16987  tgtopon  17028  indistopon  17057  clsval2  17106  opncldf1  17140  mretopd  17148  toponmre  17149  neiptopuni  17186  neiptopreu  17189  restopnb  17231  ordtcnv  17257  lecldbas  17275  ordtrestixx  17278  iscncl  17325  cnprest  17345  pnrmopn  17399  ordtt1  17435  2ndcctbss  17510  kgenval  17559  elptr  17597  ptunimpt  17619  ptpjopn  17636  ptcld  17637  hausdiag  17669  qtopeu  17740  pt1hmeo  17830  ptuncnv  17831  ptunhmeo  17832  qtophmeo  17841  ufileu  17943  elfm3  17974  rnelfmlem  17976  fmfnfmlem3  17980  flffval  18013  isfcls  18033  ptcmplem5  18079  prdstmdd  18145  prdstgpd  18146  utopbas  18257  restutopopn  18260  ustuqtop1  18263  ustuqtop3  18265  ustuqtop5  18267  blfvalps  18405  setsms  18502  imasf1oxms  18511  stdbdmopn  18540  isngp4  18650  nmrtri  18662  nminvr  18697  lssnlm  18728  cnmet  18798  metds0  18872  metdstri  18873  metdseq0  18876  xrhmeo  18963  icccvx  18967  pcoass  19041  pcorevlem  19043  pcophtb  19046  elpi1i  19063  pi1xfr  19072  pi1xfrcnvlem  19073  lmhmclm  19103  clmmulg  19110  zlmclm  19112  clmzlmvsca  19113  tchcph  19186  cmetss  19259  pmltpclem2  19338  elovolmr  19364  iundisj2  19435  voliunlem1  19436  iunmbl2  19443  ioombl1lem4  19447  uniioombllem3  19469  uniioombllem4  19470  uniioombllem6  19472  dyadmaxlem  19481  volivth  19491  vitalilem3  19494  mbfsub  19546  mbfsup  19548  itg1addlem4  19583  itg1mulc  19588  mbfi1fseqlem6  19604  itgfsum  19710  itgsplitioo  19721  dvaddf  19820  dvexp  19831  dvcnvlem  19852  dvexp3  19854  dveflem  19855  rolle  19866  dvlip  19869  lhop1lem  19889  dvfsumlem1  19902  dvfsumlem3  19904  tdeglem4  19975  tdeglem2  19976  deg1suble  20022  ply1divalg2  20053  facth1  20079  fta1glem1  20080  dvply2g  20194  plydivlem3  20204  fta1lem  20216  quotcan  20218  aaliou3lem7  20258  aaliou3  20260  dvntaylp  20279  ulm2  20293  ulmclm  20295  ulmuni  20300  mtest  20312  mbfulm  20314  pserulm  20330  abelthlem3  20341  abelthlem8  20347  reeff1o  20355  coseq0negpitopi  20403  abssinper  20418  sineq0  20421  cosord  20426  efiarg  20494  abslogle  20505  logdivlt  20508  logcnlem4  20528  logtayl  20543  dvcxp1  20618  dvcxp2  20619  sqrcn  20626  cxpeq  20633  ang180lem2  20644  ang180lem3  20645  logrec  20653  isosctrlem2  20655  isosctrlem3  20656  angpieqvd  20664  dcubic2  20676  cubic2  20680  dquartlem2  20684  dquart  20685  asinlem3  20703  atans2  20763  rlimcnp  20796  rlimcnp2  20797  amgmlem  20820  ftalem5  20851  dvdsppwf1o  20963  sgmmul  20977  perfect  21007  bcmono  21053  efexple  21057  bposlem1  21060  bposlem9  21068  lgsvalmod  21091  lgsneg  21095  lgsdchrval  21123  lgsquadlem2  21131  chtppilimlem1  21159  rpvmasumlem  21173  dchrisumlema  21174  dchrisumlem2  21176  dchrmusum2  21180  dchrvmasumlem1  21181  dchrvmasum2lem  21182  dchrvmasum2if  21183  dchrvmasumiflem1  21187  dchrisum0fmul  21192  dchrisum0lem2  21204  rplogsum  21213  selberg2lem  21236  logdivbnd  21242  pntrsumo1  21251  selberg3r  21255  selberg4r  21256  selberg34r  21257  pntrlog2bndlem2  21264  pntrlog2bndlem4  21266  qrngdiv  21310  umgraex  21350  nbgraop  21428  cusgrasizeinds  21477  cusgrasize2inds  21478  cusgrafilem2  21481  uvtxnbgra  21494  0wlkon  21539  redwlk  21598  fargshiftlem  21613  fargshiftfo  21617  fargshiftfva  21618  dfconngra1  21650  eupatrl  21682  eupath2  21694  isgrpo  21776  isgrpoi  21778  grpoidinvlem2  21785  grpoinvid2  21811  grpoinvf  21820  isgrpda  21877  subgoinv  21888  exidu1  21906  cmpidelt  21909  ablomul  21935  rngoideu  21964  rngo2  21968  rngolz  21981  rngorz  21982  rngmgmbs4  21997  rngorn1eq  22000  rngosn3  22006  nvmtri2  22153  dipcj  22205  sspg  22219  ssps  22221  sspn  22227  nmlno0lem  22286  cncph  22312  ipasslem2  22325  siii  22346  ubthlem1  22364  ubthlem2  22365  hlipcj  22405  hiidge0  22592  bcseqi  22614  shuni  22794  shunssi  22862  pjhthlem2  22886  shlub  22908  pjop  22921  pjpo  22922  h1de2i  23047  fh1  23112  fh2  23113  chscllem2  23132  chscllem3  23133  pjo  23165  pjcji  23178  hmopre  23418  adjvalval  23432  hmopadj  23434  hmoplin  23437  idhmop  23477  nmlnop0iALT  23490  nmopun  23509  cnvbraval  23605  bracnlnval  23609  kbass3  23613  pjhmopi  23641  hstoh  23727  sto2i  23732  atom1d  23848  atcv0eq  23874  atcv1  23875  ifeqeqx  23993  ifbieq12d2  23994  iundisj2f  24022  imadifxp  24030  ofresid  24047  fmptcof2  24068  xlt2addrd  24116  iundisj2fi  24145  ofldchr  24236  redvr  24269  xrge0pluscn  24318  qqhval2lem  24357  qqhval2  24358  rrhcn  24372  logbrec  24397  indf1ofs  24415  esumel  24434  esumc  24438  gsumesum  24443  esumfsup  24452  esumfsupre  24453  esumpfinvallem  24456  esumpcvgval  24460  esumpmono  24461  esumcocn  24462  unisg  24518  voliune  24577  volfiniune  24578  probmeasb  24680  ballotlemfp1  24741  ballotlemsf1o  24763  ballotlemrinv0  24782  zetacvg  24791  lgamgulmlem2  24806  lgamgulmlem3  24807  lgamcvg2  24831  gamcvg2lem  24835  subfacp1lem5  24862  subfacval2  24865  subfacval3  24867  conpcon  24914  sconpi1  24918  relexpcnv  25125  relexpadd  25130  rtrclreclem.trans  25138  dfrtrcl2  25140  clim2div  25209  fprodcvg  25248  fprodss  25266  fprodser  25267  fprodconst  25294  fprodcom2  25300  iprodfac  25358  tfisg  25471  wfr3g  25529  tfr3ALT  25552  frr3g  25573  nofnbday  25599  sltres  25611  nodense  25636  colinearalglem2  25838  ax5seglem9  25868  axpaschlem  25871  axpasch  25872  axcontlem7  25901  fvtransport  25958  transportprops  25960  btwnconn1lem12  26024  midofsegid  26030  outsideofeq  26056  lineunray  26073  bpolysum  26091  fsumcube  26098  rankeq1o  26104  onsuctopon  26176  supaddc  26228  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  itg2addnclem  26246  itg2addnc  26249  ftc1anclem5  26274  ftc1anclem7  26276  areacirclem2  26282  areacirclem5  26286  nn0prpwlem  26316  opnbnd  26319  cldbnd  26320  refssfne  26365  fnejoin2  26389  sdclem2  26437  trirn  26448  isbnd2  26483  ghomdiv  26550  rngogrphom  26578  0rngo  26628  prnc  26668  isdmn3  26675  prtlem11  26706  elrfi  26739  elrfirn  26740  mapfzcons  26763  mzprename  26797  eldioph2b  26812  lzenom  26819  diophin  26822  eq0rabdioph  26826  rexrabdioph  26845  rexzrexnn0  26855  fphpdo  26869  irrapxlem2  26877  irrapxlem3  26878  irrapxlem5  26880  pellexlem2  26884  pellexlem6  26888  pell1234qrdich  26915  pell14qrdich  26923  pell1qrge1  26924  pell1qrgaplem  26927  pellfund14gap  26941  qirropth  26962  rmxyelqirr  26964  rmxycomplete  26971  rmxy1  26976  rmym1  26989  rmxluc  26990  rmxdbl  26993  acongtr  27034  jm2.18  27050  jm2.22  27057  jm2.23  27058  jm2.25  27061  jm2.26lem3  27063  jm2.27a  27067  jm2.27c  27069  fnwe2lem3  27118  kelac1  27129  pwssplit4  27159  filnm  27160  pwslnmlem2  27163  frlmpws  27186  frlmlss  27187  frlmlbs  27217  frlmup3  27220  ellspd  27222  unxpwdom3  27224  imasgim  27232  isnumbasgrplem3  27238  lsslindf  27268  islindf4  27276  islindf5  27277  hbt  27302  mpaaeu  27323  rngunsnply  27346  en2eleq  27349  pmtrfrn  27368  psgnunilem1  27384  hashgcdlem  27484  proot1ex  27488  ofdivrec  27511  iotaexeu  27586  iotasbc  27587  pm14.24  27600  sbiota1  27602  cncmpmax  27670  refsum2cnlem1  27675  expcnfg  27693  clim1fr1  27694  isumneg  27695  climneg  27703  climdivf  27705  itgsin0pilem1  27711  ibliccsinexp  27712  itgsinexplem1  27715  itgsinexp  27716  stoweidlem2  27718  stoweidlem3  27719  stoweidlem13  27729  stoweidlem19  27735  stoweidlem21  27737  stoweidlem24  27740  stoweidlem26  27742  stoweidlem29  27745  stoweidlem40  27756  stoweidlem42  27758  stoweidlem62  27778  wallispilem4  27784  wallispi  27786  wallispi2lem1  27787  wallispi2lem2  27788  stirlinglem1  27790  stirlinglem3  27792  stirlinglem4  27793  stirlinglem5  27794  stirlinglem6  27795  stirlinglem7  27796  stirlinglem8  27797  stirlinglem10  27799  stirlinglem12  27801  stirlinglem15  27804  sigaras  27812  sigarms  27813  sigarperm  27817  sharhght  27822  afvelrn  27999  afvres  28003  dmfcoafv  28006  afvco2  28007  2if2  28043  resisresindm  28061  imarnf1pr  28070  fzosplitsnm1  28114  flpmodeq  28128  modifeq2int  28139  ccatsymb  28152  swrd0swrd  28163  swrdswrd  28165  swrdswrd0  28167  swrdccatfn  28170  swrdccatin12lem3b  28175  swrdccatin12lem3  28178  swrdccat3blem  28184  swrdccat3b  28185  modprm1div  28190  reumodprminv  28193  cshwidx  28208  cshwidxmod  28209  2cshw2lem3  28220  2cshwmod  28223  cshwleneq  28231  3cshw  28232  cshweqdif2  28233  cshwssizelem4a  28246  usgra2adedgwlk  28269  usg2spthonot  28308  usg2spthonot0  28309  frgraunss  28322  frgrancvvdeqlem4  28359  frg2woteq  28386  onetansqsecsq  28441  csbsngVD  28942  isosctrlem1ALT  28983  sineq0ALT  28986  bnj1241  29116  bnj548  29205  lsatel  29740  lsatfixedN  29744  lsat0cv  29768  ldualgrplem  29880  lduallmodlem  29887  lkrpssN  29898  lkreqN  29905  omlfh1N  29993  atcvreq0  30049  glbconN  30111  2atjm  30179  hlatexch3N  30214  lplnexllnN  30298  2llnjaN  30300  2lplnja  30353  dalem56  30462  2llnma1b  30520  atmod1i1  30591  atmod1i2  30593  llnmod1i2  30594  dalawlem11  30615  pclfinN  30634  osumclN  30701  4atexlemswapqr  30797  4atexlemunv  30800  cdleme15a  31008  cdleme16  31019  cdleme22cN  31076  cdleme22d  31077  cdleme43dN  31226  cdlemeg46sfg  31254  cdlemeg46fjgN  31255  cdlemg1a  31304  cdlemeiota  31319  cdlemg3a  31331  cdlemg12e  31381  cdlemg18a  31412  trlcone  31462  tgrpgrplem  31483  tgrpabl  31485  cdlemk4  31568  cdlemksv2  31581  cdlemkuv2  31601  cdlemk19  31603  cdlemk22  31627  cdlemk53a  31689  erngdvlem1  31722  erngdvlem2N  31723  erngdvlem3  31724  erngdvlem4  31725  erngdvlem1-rN  31730  erngdvlem2-rN  31731  erngdvlem3-rN  31732  erngdvlem4-rN  31733  dvalveclem  31760  dialss  31781  dia2dimlem2  31800  dia2dimlem3  31801  dvhgrp  31842  dvhlveclem  31843  cdlemm10N  31853  doca2N  31861  diblss  31905  dicvaddcl  31925  dicvscacl  31926  dicn0  31927  diclss  31928  cdlemn11a  31942  dihjust  31952  dihopelvalcpre  31983  dihmeetlem5  32043  dochlkr  32120  dihsmatrn  32171  dvh4dimat  32173  mapdval4N  32367  mapdcv  32395  mapdpglem15  32421  baerlem5bmN  32452  baerlem5abmN  32453  mapdh8aa  32511  hdmapval3lemN  32575  hdmap10lem  32577  hdmaprnlem10N  32597  hdmap14lem2a  32605  hdmap14lem2N  32607  hdmap14lem3  32608  hdmap14lem6  32611  hgmapvs  32629  hlhilocv  32695  hlhillcs  32696
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-cleq 2428
  Copyright terms: Public domain W3C validator