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

Theorem 3eqtr4g 2882
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 2869 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4g.3 . 2 𝐷 = 𝐵
53, 4eqtr4di 2875 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2815
This theorem is referenced by:  rabbidva2  3451  rabeqf  3456  rabeqiOLD  3458  csbeq1  3858  csbeq2  3860  csbeq2d  3861  difeq1  4067  difeq2  4068  uneq2  4108  ineq1  4155  ineq2  4157  symdifeq1  4195  symdifeq2  4196  dfrab3ss  4255  csbprc  4330  csbnestgfw  4343  csbnestgf  4348  disjssun  4389  ifeq1  4443  ifeq2  4444  pweqALT  4528  sneq  4549  csbsng  4618  csbprg  4619  preq1  4643  preq2  4644  tpeq1  4652  tpeq2  4653  tpeq3  4654  prprc1  4675  tpprceq3  4710  opeq1  4776  opeq1OLD  4777  opeq2  4778  opeq2OLD  4779  oteq1  4787  oteq2  4788  oteq3  4789  csbopg  4796  unieqOLD  4825  csbuni  4842  inteq  4854  iineq1  4911  iineq2  4914  iuneq12df  4920  dfiin2g  4932  iinrab  4966  iinin1  4976  iinxprg  4986  iununi  4996  opabbid  5107  mpteq12df  5124  mpteq12f  5125  csbmpt12  5421  xpeq1  5546  xpeq2  5553  rneq  5783  reseq1  5825  reseq2  5826  resima2  5866  resindm  5878  resmpt  5883  resmptf  5885  imaeq1  5902  imaeq2  5903  mptcnv  5976  xpdisj1  5996  xpdisj2  5997  resdisj  6004  dmpropg  6050  rnpropg  6057  cores  6080  cores2  6090  xpco  6118  predeq123  6127  sspred  6134  suceq  6234  sucprc  6244  iotaeq  6305  iotabi  6306  fntpg  6393  imain  6418  f1oprswap  6640  fveq1  6651  fveq2  6652  fvres  6671  csbfv12  6695  fnimapr  6729  fvco2  6740  xpprsng  6884  residpr  6887  fsnunfv  6931  fsnunres  6932  funiunfv  6990  fliftf  7052  isoini2  7076  riotaeqdv  7099  riotabidv  7100  riotauni  7104  riotabidva  7117  snriota  7131  oveq  7146  oveq1  7147  oveq2  7148  oprabbid  7203  mpoeq123  7210  mpoeq123dva  7212  mpoeq3dva  7215  resmpo  7256  ovres  7299  f1ocnvd  7381  ofeq  7396  ofreq  7397  fpar  7798  wrecseq123  7935  onovuni  7966  recseq  7997  tfr2a  8018  rdgeq1  8034  rdgeq2  8035  rdgsucmptf  8051  frsucmpt  8060  seqomeq12  8077  seqomsuc  8080  omopthi  8271  eceq1  8314  eceq2  8316  qseq1  8330  qseq2  8331  uniqs  8344  ecinxp  8359  qsinxp  8360  erovlem  8380  ecopovtrn  8387  ixpeq1  8459  supeq1  8897  supeq2  8900  supeq3  8901  supeq123d  8902  infeq1  8928  infeq2  8931  infeq3  8932  infeq123d  8933  infiso  8960  oieq1  8964  oieq2  8965  ordtypelem1  8970  inf3lemc  9077  wemapwe  9148  r1sucg  9186  r1limg  9188  rankprb  9268  karden  9312  djueq12  9321  cardiun  9399  acneq  9458  alephlim  9482  alephsuc  9483  alephfplem2  9520  infpssrlem2  9715  fin23lem34  9757  fin23lem35  9758  zorn2lem1  9907  zorn2lem7  9913  fpwwe2lem6  10046  fpwwe2lem13  10053  addpiord  10295  mulpiord  10296  addpqnq  10349  mulpqnq  10352  addassnq  10369  mulassnq  10370  distrnq  10372  lterpq  10381  ltexnq  10386  ltsrpr  10488  00sr  10510  recexsrlem  10514  mulgt0sr  10516  addcnsrec  10554  mulcnsrec  10555  negeq  10867  csbnegg  10872  negsubdi  10931  mulneg1  11065  negfi  11577  deceq1  12091  deceq2  12092  xnegeq  12588  fseq1p1m1  12976  om2uzrdg  13319  uzrdgsuci  13323  seqeq1  13367  seqeq2  13368  seqeq3  13369  seqfeq4  13415  seqof  13423  hashprg  13752  hashtpg  13839  csbwrdg  13887  s1eq  13945  cats1co  14209  s2eqd  14216  s3eqd  14217  s4eqd  14218  s5eqd  14219  s6eqd  14220  s7eqd  14221  s8eqd  14222  xpcogend  14325  shftval  14424  limsupgle  14825  lo1eq  14916  rlimeq  14917  sumeq1  15036  sumeq2w  15040  sumeq2ii  15041  zsum  15066  sumss2  15074  fsumsplitsnun  15101  isumclim3  15105  fsumcom2  15120  incexclem  15182  incexc2  15184  isumshft  15185  prodeq1f  15253  prodeq2w  15257  prodeq2ii  15258  zprod  15282  fprodm1s  15315  fprodp1s  15316  fprodcom2  15329  fprodsplitf  15333  iprodclim3  15345  ef0lem  15423  ruclem7  15580  sadcp1  15793  smupp1  15818  smueqlem  15828  algrp1  15907  dfphi2  16100  prmdiveq  16112  pceulem  16171  vdwlem6  16311  cshwsiun  16424  sloteq  16479  setsid  16529  elbasfv  16535  elbasov  16536  imastset  16786  imasvscaval  16802  isoval  17026  funcoppc  17136  fulloppc  17183  fuccofval  17220  natpropd  17237  catccofval  17351  xpchomfval  17420  xpccofval  17423  lubfval  17579  glbfval  17592  grpidpropd  17863  gsumpropd2lem  17880  frmdplusg  18010  efmndplusg  18036  grpinvpropd  18165  grpsubpropd  18195  grpsubpropd2  18196  mulgpropd  18260  oppgmnd  18473  sylow1lem2  18715  sylow3lem1  18743  prds1  19358  pwsmgp  19362  opprring  19375  rngidpropd  19439  dvdsrpropd  19440  unitpropd  19441  invrpropd  19442  rhm1  19476  lmhmpropd  19836  lidlrsppropd  19994  lpival  20009  zrhpropd  20206  znle  20226  frlmplusgval  20451  frlmvscafval  20453  ressascl  20580  asclpropd  20581  aspval2  20582  psrbas  20614  psrplusg  20617  psrmulr  20620  psrvscafval  20626  resspsrbas  20651  ressmplbas2  20693  opsrle  20713  opsrbaslem  20715  vr1val  20819  ressply1add  20857  ressply1mul  20858  ressply1vsca  20859  psrplusgpropd  20863  mplbaspropd  20864  psropprmul  20865  ply1baspropd  20870  ply1plusgpropd  20871  ply1sca2  20881  subrgvr1  20888  coe1mul2lem2  20895  ply1coe1eq  20925  mamudi  21006  mamudir  21007  matrcl  21015  oftpos  21055  mattpos1  21059  mdetfval  21189  mdetrlin  21205  mdetrsca  21206  mdetrsca2  21207  mdetrlin2  21210  mdetunilem5  21219  madufval  21240  madugsum  21246  idmatidpmat  21340  cpmidpmat  21476  cncmp  21995  2ndcsep  22062  llyeq  22073  nllyeq  22074  xkouni  22202  hmphindis  22400  xkocnv  22417  ptcmplem2  22656  snclseqg  22719  prdstmdd  22727  ustexsym  22819  ucnextcn  22908  metreslem  22967  comet  23118  nrmmetd  23179  nmpropd  23198  isngp3  23202  ngpds  23208  subgnm  23237  tngnm  23255  idnghm  23347  cnmetdval  23374  cnmpopc  23531  htpyco2  23582  phtpyco2  23593  clsocv  23852  rrxprds  23991  rrxnm  23993  rrxplusgvscavalb  23997  ovolunlem1a  24098  voliunlem3  24154  ioombl1lem4  24163  uniioombllem4  24188  itg11  24293  itgeq1f  24373  itgeq2  24379  iblss2  24407  itgss  24413  itgeqa  24415  itgfsum  24428  itgsplit  24437  ditgeq1  24449  ditgeq2  24450  ditgeq3  24451  dvcmulf  24546  dvmptfsum  24576  dvcnvrelem2  24619  mdegfval  24661  mdegpropd  24683  deg1propd  24685  plyeq0  24806  coe11  24848  dgrlt  24861  dgradd2  24863  dgrmulc  24866  dvply1  24878  fta1lem  24901  pserulm  25015  rlimcnp2  25550  jensenlem1  25570  basellem5  25668  dchrbas  25817  dchrrcl  25822  dchrplusg  25829  dchrfi  25837  lgsdi  25916  lgseisenlem2  25958  lgsquadlem3  25964  dchrmusumlema  26075  rpvmasum2  26094  dchrisum0lema  26096  pntlemg  26180  colperpexlem2  26523  axlowdimlem13  26746  uhgrvtxedgiedgb  26927  nb3grprlem1  27168  crctcshlem2  27602  wpthswwlks2on  27745  clwlknf1oclwwlkn  27867  frgrncvvdeq  28092  avril1  28246  0vfval  28387  imsval  28466  imsdval  28467  bcseqi  28901  normpythi  28923  cm0  29390  fh1  29399  pjcji  29465  opsqrlem5  29925  pjsdi2i  29938  pjclem3  29978  pjci  29981  golem1  30052  iuneq12daf  30315  iunrdx  30322  ofresid  30397  fnimatp  30431  cnvprop  30440  coprprop  30443  f1od2  30467  dp2eq1  30559  dp2eq2  30560  fzto1st1  30775  gsumvsca1  30885  gsumvsca2  30886  rhmopp  30924  resv1r  30942  lindsunlem  31077  fedgmullem1  31082  fedgmullem2  31083  fedgmul  31084  crefeq  31167  rspectopn  31189  xrge0mulc1cn  31258  qqhval2  31297  esumeq12dvaf  31364  esumeq2  31369  esumf1o  31383  esumfzf  31402  esumss  31405  esumpfinvalf  31409  ofceq  31430  carsgclctunlem1  31649  itgeq12dv  31658  ccatmulgnn0dir  31886  breprexpnat  31979  bnj956  32122  bnj1385  32178  bnj96  32211  bnj548  32243  bnj553  32244  bnj554  32245  bnj602  32261  bnj18eq1  32273  bnj1234  32359  bnj1296  32367  bnj1318  32371  bnj1442  32395  bnj1450  32396  cvmliftlem5  32610  cvmliftlem10  32615  cvmlift2lem9  32632  cvmliftphtlem  32638  satfdm  32690  mthmpps  32903  eqfunressuc  33079  rdgprc  33113  dfrdg2  33114  trpredeq1  33133  trpredeq2  33134  trpredeq3  33135  wsuceq123  33175  wlimeq12  33180  frecseq123  33193  nosupbnd2lem1  33289  altopthsn  33496  altxpeq1  33508  altxpeq2  33509  ee7.2aOLD  33883  bj-rabbida2  34322  bj-sngleq  34364  bj-tageq  34373  bj-projeq  34389  bj-projval  34393  bj-1upleq  34396  bj-pr1eq  34399  bj-pr2eq  34413  bj-evaleq  34448  bj-imafv  34627  bj-isrvec  34669  csbpredg  34704  csbwrecsg  34705  csbrecsg  34706  csbrdgg  34707  csboprabg  34708  csbmpo123  34709  finxpeq1  34764  finxpeq2  34765  csbfinxpg  34766  finxpreclem4  34772  cureq  34992  unceq  34993  uncov  34997  unccur  34999  finixpnum  35001  ptrest  35015  poimirlem3  35019  poimirlem9  35025  poimirlem15  35031  poimirlem16  35032  poimirlem26  35042  poimirlem27  35043  mbfposadd  35063  cnambfre  35064  iblabsnclem  35079  ftc1anclem1  35089  heiborlem4  35211  heiborlem6  35213  mpobi123f  35559  iineq12f  35561  mptbi12f  35563  eccnvepres  35656  uniqsALTV  35705  xrneq1  35748  xrneq2  35751  cosseq  35790  redundss3  35982  riotaclbgBAD  36209  toycom  36228  ldualvbase  36381  ldualfvadd  36383  ldualsca  36387  ldualsbase  36388  ldualsaddN  36389  ldualfvs  36391  ldual0  36402  ldual1  36403  ldualneg  36404  cdleme19f  37563  cdleme20m  37578  cdleme21k  37593  cdleme27b  37623  cdleme31so  37634  cdleme31sn  37635  cdleme31se  37637  cdleme31se2  37638  cdleme31sc  37639  cdleme31sde  37640  cdleme31fv  37645  cdleme40v  37724  cdleme43dN  37747  cdlemeg46ngfr  37773  ltrnco4  37994  tgrpbase  38001  tgrpopr  38002  erngbase  38056  erngfplus  38057  erngfmul  38060  erngbase-rN  38064  erngfplus-rN  38065  erngfmul-rN  38068  dvasca  38261  dvavbase  38268  dvafvadd  38269  dvafvsca  38271  tendocnv  38276  dvhsca  38337  dvhfplusr  38339  dvhvbase  38342  dvhfvadd  38346  dvhfvsca  38355  lcdvadd  38852  lcdsbase  38855  lcdsadd  38856  lcdvs  38858  lcd0  38863  lcd1  38864  lcdneg  38865  fsuppind  39404  prjspnval2  39542  imaiinfv  39565  mapfzcons1  39589  rexrabdioph  39666  dnnumch1  39919  dnwech  39923  aomclem6  39934  pwssplit4  39964  pwfi2f1o  39971  mendplusgfval  40060  mendvscafval  40065  harval3  40175  dssmapntrcls  40765  scotteqd  40880  colleq12d  40896  uzmptshftfval  40985  dropab1  41086  dropab2  41087  rabbida2  41705  rabbida3  41708  itgsinexplem1  42536  wallispi2lem2  42654  fourierdlem36  42725  etransclem4  42820  afveq12d  43629  aoveq123d  43674  aovfundmoveq  43677  aovnuoveq  43687  aovvoveq  43688  aovovn0oveq  43690  afv2eq12d  43711  fsumsplitsndif  43830  rngccofvalALTV  44551  ringccofvalALTV  44614  rhmsubclem2  44651  rhmsubcALTVlem2  44669  itscnhlinecirc02plem2  45137  setrecseq  45155  aacllem  45269
  Copyright terms: Public domain W3C validator