MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr4g Structured version   Visualization version   GIF version

Theorem 3eqtr4g 2680
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
3eqtr4g.1 (𝜑𝐴 = 𝐵)
3eqtr4g.2 𝐶 = 𝐴
3eqtr4g.3 𝐷 = 𝐵
Assertion
Ref Expression
3eqtr4g (𝜑𝐶 = 𝐷)

Proof of Theorem 3eqtr4g
StepHypRef Expression
1 3eqtr4g.2 . . 3 𝐶 = 𝐴
2 3eqtr4g.1 . . 3 (𝜑𝐴 = 𝐵)
31, 2syl5eq 2667 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4g.3 . 2 𝐷 = 𝐵
53, 4syl6eqr 2673 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704  df-cleq 2614
This theorem is referenced by:  rabbidva2  3184  rabeqf  3188  csbeq1  3534  csbeq2  3535  difeq1  3719  difeq2  3720  uneq2  3759  ineq2  3806  symdifeq1  3844  symdifeq2  3845  dfrab3ss  3903  csbprc  3978  csbeq2d  3989  csbnestgf  3994  disjssun  4034  ifeq1  4088  ifeq2  4089  pweq  4159  sneq  4185  csbsng  4241  csbprg  4242  rabsn  4254  preq1  4266  preq2  4267  tpeq1  4275  tpeq2  4276  tpeq3  4277  prprc1  4298  tpprceq3  4333  opeq1  4400  opeq2  4401  oteq1  4409  oteq2  4410  oteq3  4411  csbopg  4418  unieq  4442  csbuni  4464  inteq  4476  iineq1  4533  iineq2  4536  dfiin2g  4551  iinrab  4580  iinin1  4589  iinxprg  4599  iununi  4608  opabbid  4713  mpteq12f  4729  mpteq12d  4732  mpteq12df  4733  csbmpt12  5008  xpeq1  5126  xpeq2  5127  rneq  5349  reseq1  5388  reseq2  5389  resima2  5430  resindm  5442  resmpt  5447  resmptf  5449  imaeq1  5459  imaeq2  5460  mptcnv  5532  xpdisj1  5553  xpdisj2  5554  resdisj  5561  dmpropg  5606  rnpropg  5613  cores  5636  cores2  5646  xpco  5673  predeq123  5679  sspred  5686  suceq  5788  sucprc  5798  iotaeq  5857  iotabi  5858  fntpg  5946  imain  5972  f1oprswap  6178  fveq1  6188  fveq2  6189  fvres  6205  csbfv12  6229  fnimapr  6260  fvco2  6271  residpr  6406  fsnunfv  6450  fsnunres  6451  funiunfv  6503  fliftf  6562  isoini2  6586  riotaeqdv  6609  riotabidv  6610  riotauni  6614  riotabidva  6624  snriota  6638  oveq  6653  oveq1  6654  oveq2  6655  oprabbid  6705  mpt2eq123  6711  mpt2eq123dva  6713  mpt2eq3dva  6716  resmpt2  6755  ovres  6797  f1ocnvd  6881  ofeq  6896  ofreq  6897  fpar  7278  wrecseq123  7405  onovuni  7436  recseq  7467  tfr2a  7488  rdgeq1  7504  rdgeq2  7505  rdgsucmptf  7521  frsucmpt  7530  seqomeq12  7546  seqomsuc  7549  omopthi  7734  eceq1  7779  eceq2  7781  qseq1  7793  qseq2  7794  uniqs  7804  ecinxp  7819  qsinxp  7820  erovlem  7840  ecopovtrn  7847  ixpeq1  7916  supeq1  8348  supeq2  8351  supeq3  8352  supeq123d  8353  infeq1  8379  infeq2  8382  infeq3  8383  infeq123d  8384  infiso  8410  oieq1  8414  oieq2  8415  ordtypelem1  8420  inf3lemc  8520  wemapwe  8591  r1sucg  8629  r1limg  8631  rankprb  8711  karden  8755  cardiun  8805  acneq  8863  alephlim  8887  alephsuc  8888  alephfplem2  8925  infpssrlem2  9123  fin23lem34  9165  fin23lem35  9166  zorn2lem1  9315  zorn2lem7  9321  fpwwe2lem6  9454  fpwwe2lem13  9461  addpiord  9703  mulpiord  9704  addpqnq  9757  mulpqnq  9760  addassnq  9777  mulassnq  9778  distrnq  9780  lterpq  9789  ltexnq  9794  ltsrpr  9895  00sr  9917  recexsrlem  9921  mulgt0sr  9923  addcnsrec  9961  mulcnsrec  9962  negeq  10270  csbnegg  10275  negsubdi  10334  mulneg1  10463  negfi  10968  deceq1  11497  deceq1OLD  11498  deceq2  11499  deceq2OLD  11500  xnegeq  12035  fseq1p1m1  12410  om2uzrdg  12750  uzrdgsuci  12754  seqeq1  12799  seqeq2  12800  seqeq3  12801  seqfeq4  12845  seqof  12853  hashprg  13177  hashprgOLD  13178  hashmap  13217  hashtpg  13262  csbwrdg  13329  s1eq  13375  cats1co  13595  s2eqd  13602  s3eqd  13603  s4eqd  13604  s5eqd  13605  s6eqd  13606  s7eqd  13607  s8eqd  13608  xpcogend  13707  shftval  13808  limsupgle  14202  lo1eq  14293  rlimeq  14294  sumeq1  14413  sumeq2w  14416  sumeq2ii  14417  zsum  14443  sumss2  14451  fsumsplitsnun  14478  fsumsplitsnunOLD  14480  isumclim3  14484  fsumcom2  14499  fsumcom2OLD  14500  incexclem  14562  incexc2  14564  isumshft  14565  prodeq1f  14632  prodeq2w  14636  prodeq2ii  14637  zprod  14661  fprodm1s  14694  fprodp1s  14695  fprodcom2  14708  fprodcom2OLD  14709  iprodclim3  14725  ef0lem  14803  ruclem7  14959  sadcp1  15171  smupp1  15196  smueqlem  15206  algrp1  15281  dfphi2  15473  prmdiveq  15485  pceulem  15544  vdwlem6  15684  cshwsiun  15800  sloteq  15856  setsid  15908  elbasfv  15914  elbasov  15915  imastset  16176  imasvscaval  16192  xpscg  16212  isoval  16419  funcoppc  16529  fulloppc  16576  fuccofval  16613  natpropd  16630  catccofval  16744  xpchomfval  16813  xpccofval  16816  lubfval  16972  glbfval  16985  grpidpropd  17255  gsumpropd2lem  17267  frmdplusg  17385  grpinvpropd  17484  grpsubpropd  17514  grpsubpropd2  17515  mulgpropd  17578  oppgmnd  17778  symgplusg  17803  sylow1lem2  18008  sylow3lem1  18036  prds1  18608  pwsmgp  18612  opprring  18625  rngidpropd  18689  dvdsrpropd  18690  unitpropd  18691  invrpropd  18692  rhm1  18724  lmhmpropd  19067  lidlrsppropd  19224  lpival  19239  ressascl  19338  asclpropd  19340  aspval2  19341  psrbas  19372  psrplusg  19375  psrmulr  19378  psrvscafval  19384  resspsrbas  19409  ressmplbas2  19449  opsrle  19469  opsrbaslem  19471  opsrbaslemOLD  19472  vr1val  19556  ressply1add  19594  ressply1mul  19595  ressply1vsca  19596  psrplusgpropd  19600  mplbaspropd  19601  psropprmul  19602  ply1baspropd  19607  ply1plusgpropd  19608  ply1sca2  19618  subrgvr1  19625  coe1mul2lem2  19632  ply1coe1eq  19662  zrhpropd  19857  znle  19878  frlmplusgval  20101  frlmvscafval  20103  mamudi  20203  mamudir  20204  matrcl  20212  oftpos  20252  mattpos1  20256  mdetfval  20386  mdetrlin  20402  mdetrsca  20403  mdetrsca2  20404  mdetrlin2  20407  mdetunilem5  20416  madufval  20437  madugsum  20443  idmatidpmat  20536  cpmidpmat  20672  cncmp  21189  2ndcsep  21256  llyeq  21267  nllyeq  21268  xkouni  21396  hmphindis  21594  xkocnv  21611  ptcmplem2  21851  snclseqg  21913  prdstmdd  21921  ustexsym  22013  ucnextcn  22102  metreslem  22161  comet  22312  nrmmetd  22373  nmpropd  22392  isngp3  22396  ngpds  22402  subgnm  22431  tngnm  22449  idnghm  22541  cnmetdval  22568  cnmpt2pc  22721  htpyco2  22772  phtpyco2  22783  clsocv  23043  rrxprds  23171  rrxnm  23173  ovolunlem1a  23258  voliunlem3  23314  ioombl1lem4  23323  uniioombllem4  23348  itg11  23452  itgeq1f  23532  itgeq2  23538  iblss2  23566  itgss  23572  itgeqa  23574  itgfsum  23587  itgsplit  23596  ditgeq1  23606  ditgeq2  23607  ditgeq3  23608  dvcmulf  23702  dvmptfsum  23732  dvcnvrelem2  23775  mdegfval  23816  mdegpropd  23838  deg1propd  23840  plyeq0  23961  coe11  24003  dgrlt  24016  dgradd2  24018  dgrmulc  24021  dvply1  24033  fta1lem  24056  pserulm  24170  rlimcnp2  24687  jensenlem1  24707  basellem5  24805  dchrbas  24954  dchrrcl  24959  dchrplusg  24966  dchrfi  24974  lgsdi  25053  lgseisenlem2  25095  lgsquadlem3  25101  dchrmusumlema  25176  rpvmasum2  25195  dchrisum0lema  25197  pntlemg  25281  colperpexlem2  25617  axlowdimlem13  25828  uhgrvtxedgiedgb  26025  nb3grprlem1  26276  crctcshlem2  26704  frgrncvvdeq  27166  avril1  27303  0vfval  27445  imsval  27524  imsdval  27525  bcseqi  27961  normpythi  27983  cm0  28452  fh1  28461  pjcji  28527  opsqrlem5  28987  pjsdi2i  29000  pjclem3  29040  pjci  29043  golem1  29114  iunrdx  29366  ofresid  29428  f1od2  29484  dp2eq1  29565  dp2eq2  29566  gsumvsca1  29767  gsumvsca2  29768  rhmopp  29804  resv1r  29822  fzto1st1  29837  crefeq  29897  xrge0mulc1cn  29972  qqhval2  30011  esumeq12dvaf  30078  esumeq2  30083  esumf1o  30097  esumfzf  30116  esumss  30119  esumpfinvalf  30123  ofceq  30144  carsgclctunlem1  30364  itgeq12dv  30373  ccatmulgnn0dir  30604  breprexpnat  30697  bnj956  30832  bnj1385  30888  bnj96  30920  bnj548  30952  bnj553  30953  bnj554  30954  bnj602  30970  bnj18eq1  30982  bnj1234  31066  bnj1296  31074  bnj1318  31078  bnj1442  31102  bnj1450  31103  cvmliftlem5  31256  cvmliftlem10  31261  cvmlift2lem9  31278  cvmliftphtlem  31284  mthmpps  31464  eqfunressuc  31646  rdgprc  31684  dfrdg2  31685  trpredeq1  31704  trpredeq2  31705  trpredeq3  31706  wsuceq123  31744  wlimeq12  31749  nosupbnd2lem1  31845  altopthsn  32052  altxpeq1  32064  altxpeq2  32065  ee7.2aOLD  32444  bj-rabbida2  32897  bj-sngleq  32939  bj-tageq  32948  bj-projeq  32964  bj-projval  32968  bj-1upleq  32971  bj-pr1eq  32974  bj-pr2eq  32988  bj-evaleq  33008  csbpredg  33152  csbwrecsg  33153  csbrecsg  33154  csbrdgg  33155  csboprabg  33156  csbmpt22g  33157  finxpeq1  33203  finxpeq2  33204  csbfinxpg  33205  finxpreclem4  33211  cureq  33365  unceq  33366  uncov  33370  unccur  33372  finixpnum  33374  ptrest  33388  poimirlem3  33392  poimirlem9  33398  poimirlem15  33404  poimirlem16  33405  poimirlem26  33415  poimirlem27  33416  mbfposadd  33437  cnambfre  33438  iblabsnclem  33453  ftc1anclem1  33465  heiborlem4  33593  heiborlem6  33595  mpt2bi123f  33951  iineq12f  33953  mptbi12f  33955  riotaclbgBAD  34066  toycom  34086  ldualvbase  34239  ldualfvadd  34241  ldualsca  34245  ldualsbase  34246  ldualsaddN  34247  ldualfvs  34249  ldual0  34260  ldual1  34261  ldualneg  34262  cdleme19f  35422  cdleme20m  35437  cdleme21k  35452  cdleme27b  35482  cdleme31so  35493  cdleme31sn  35494  cdleme31se  35496  cdleme31se2  35497  cdleme31sc  35498  cdleme31sde  35499  cdleme31fv  35504  cdleme40v  35583  cdleme43dN  35606  cdlemeg46ngfr  35632  ltrnco4  35853  tgrpbase  35860  tgrpopr  35861  erngbase  35915  erngfplus  35916  erngfmul  35919  erngbase-rN  35923  erngfplus-rN  35924  erngfmul-rN  35927  dvasca  36120  dvavbase  36127  dvafvadd  36128  dvafvsca  36130  tendocnv  36136  dvhsca  36197  dvhfplusr  36199  dvhvbase  36202  dvhfvadd  36206  dvhfvsca  36215  lcdvadd  36712  lcdsbase  36715  lcdsadd  36716  lcdvs  36718  lcd0  36723  lcd1  36724  lcdneg  36725  imaiinfv  37082  mapfzcons1  37106  rexrabdioph  37184  dnnumch1  37440  dnwech  37444  aomclem6  37455  pwssplit4  37485  pwfi2f1o  37492  mendplusgfval  37581  mendvscafval  37586  dssmapntrcls  38252  uzmptshftfval  38371  dropab1  38477  dropab2  38478  csbunigOLD  38877  csbfv12gALTOLD  38878  csbxpgOLD  38879  csbresgOLD  38881  csbrngOLD  38882  csbima12gALTOLD  38883  rabbida2  39143  rabbida3  39146  itgsinexplem1  39938  wallispi2lem2  40058  fourierdlem36  40129  etransclem4  40224  afveq12d  40982  aoveq123d  41027  aovfundmoveq  41030  aovnuoveq  41040  aovvoveq  41041  aovovn0oveq  41043  fsumsplitsndif  41113  rngccofvalALTV  41758  ringccofvalALTV  41821  rhmsubclem2  41858  rhmsubcALTVlem2  41876  xpprsng  41881  setrecseq  42203  aacllem  42318
  Copyright terms: Public domain W3C validator