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

Theorem 3eqtr4g 2863
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 2850 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4g.3 . 2 𝐷 = 𝐵
53, 4syl6eqr 2856 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2782
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2797
This theorem is referenced by:  rabbidva2  3374  rabeqf  3378  csbeq1  3729  csbeq2  3730  difeq1  3918  difeq2  3919  uneq2  3958  ineq2  4005  symdifeq1  4042  symdifeq2  4043  dfrab3ss  4104  csbprc  4176  csbeq2d  4186  csbnestgf  4191  disjssun  4230  ifeq1  4281  ifeq2  4282  pweq  4352  sneq  4378  csbsng  4433  csbprg  4434  preq1  4457  preq2  4458  tpeq1  4466  tpeq2  4467  tpeq3  4468  prprc1  4489  tpprceq3  4523  opeq1  4593  opeq2  4594  oteq1  4602  oteq2  4603  oteq3  4604  csbopg  4611  unieq  4636  csbuni  4658  inteq  4670  iineq1  4725  iineq2  4728  dfiin2g  4743  iinrab  4772  iinin1  4781  iinxprg  4791  iununi  4800  opabbid  4907  mpteq12f  4923  mpteq12d  4926  mpteq12df  4927  csbmpt12  5203  xpeq1  5323  xpeq2  5329  rneq  5550  reseq1  5589  reseq2  5590  resima2  5633  resindm  5647  resmpt  5652  resmptf  5654  imaeq1  5669  imaeq2  5670  mptcnv  5743  xpdisj1  5764  xpdisj2  5765  resdisj  5772  dmpropg  5818  rnpropg  5825  cores  5850  cores2  5860  xpco  5887  predeq123  5892  sspred  5899  suceq  6001  sucprc  6011  iotaeq  6070  iotabi  6071  fntpg  6158  imain  6183  f1oprswap  6394  fveq1  6405  fveq2  6406  fvres  6425  csbfv12  6449  fnimapr  6481  fvco2  6492  residpr  6630  fsnunfv  6676  fsnunres  6677  funiunfv  6728  fliftf  6787  isoini2  6811  riotaeqdv  6834  riotabidv  6835  riotauni  6839  riotabidva  6849  snriota  6863  oveq  6878  oveq1  6879  oveq2  6880  oprabbid  6936  mpt2eq123  6942  mpt2eq123dva  6944  mpt2eq3dva  6947  resmpt2  6986  ovres  7028  f1ocnvd  7112  ofeq  7127  ofreq  7128  fpar  7513  wrecseq123  7641  onovuni  7673  recseq  7704  tfr2a  7725  rdgeq1  7741  rdgeq2  7742  rdgsucmptf  7758  frsucmpt  7767  seqomeq12  7783  seqomsuc  7786  omopthi  7972  eceq1  8015  eceq2  8017  qseq1  8029  qseq2  8030  uniqs  8040  ecinxp  8055  qsinxp  8056  erovlem  8077  ecopovtrn  8084  ixpeq1  8154  supeq1  8588  supeq2  8591  supeq3  8592  supeq123d  8593  infeq1  8619  infeq2  8622  infeq3  8623  infeq123d  8624  infiso  8650  oieq1  8654  oieq2  8655  ordtypelem1  8660  inf3lemc  8768  wemapwe  8839  r1sucg  8877  r1limg  8879  rankprb  8959  karden  9003  djueq12  9012  cardiun  9089  acneq  9147  alephlim  9171  alephsuc  9172  alephfplem2  9209  infpssrlem2  9409  fin23lem34  9451  fin23lem35  9452  zorn2lem1  9601  zorn2lem7  9607  fpwwe2lem6  9740  fpwwe2lem13  9747  addpiord  9989  mulpiord  9990  addpqnq  10043  mulpqnq  10046  addassnq  10063  mulassnq  10064  distrnq  10066  lterpq  10075  ltexnq  10080  ltsrpr  10181  00sr  10203  recexsrlem  10207  mulgt0sr  10209  addcnsrec  10247  mulcnsrec  10248  negeq  10556  csbnegg  10561  negsubdi  10620  mulneg1  10749  negfi  11254  deceq1  11762  deceq2  11763  xnegeq  12254  fseq1p1m1  12635  om2uzrdg  12977  uzrdgsuci  12981  seqeq1  13025  seqeq2  13026  seqeq3  13027  seqfeq4  13071  seqof  13079  hashprg  13398  hashtpg  13482  csbwrdg  13543  s1eq  13593  cats1co  13823  s2eqd  13830  s3eqd  13831  s4eqd  13832  s5eqd  13833  s6eqd  13834  s7eqd  13835  s8eqd  13836  xpcogend  13936  shftval  14035  limsupgle  14429  lo1eq  14520  rlimeq  14521  sumeq1  14640  sumeq2w  14643  sumeq2ii  14644  zsum  14670  sumss2  14678  fsumsplitsnun  14705  fsumsplitsnunOLD  14707  isumclim3  14711  fsumcom2  14726  incexclem  14788  incexc2  14790  isumshft  14791  prodeq1f  14857  prodeq2w  14861  prodeq2ii  14862  zprod  14886  fprodm1s  14919  fprodp1s  14920  fprodcom2  14933  iprodclim3  14949  ef0lem  15027  ruclem7  15183  sadcp1  15394  smupp1  15419  smueqlem  15429  algrp1  15504  dfphi2  15694  prmdiveq  15706  pceulem  15765  vdwlem6  15905  cshwsiun  16016  sloteq  16071  setsid  16123  elbasfv  16129  elbasov  16130  imastset  16385  imasvscaval  16401  xpscg  16421  isoval  16627  funcoppc  16737  fulloppc  16784  fuccofval  16821  natpropd  16838  catccofval  16952  xpchomfval  17022  xpccofval  17025  lubfval  17181  glbfval  17194  grpidpropd  17464  gsumpropd2lem  17476  frmdplusg  17594  grpinvpropd  17693  grpsubpropd  17723  grpsubpropd2  17724  mulgpropd  17784  oppgmnd  17983  symgplusg  18008  sylow1lem2  18213  sylow3lem1  18241  prds1  18814  pwsmgp  18818  opprring  18831  rngidpropd  18895  dvdsrpropd  18896  unitpropd  18897  invrpropd  18898  rhm1  18932  lmhmpropd  19278  lidlrsppropd  19437  lpival  19452  ressascl  19551  asclpropd  19553  aspval2  19554  psrbas  19585  psrplusg  19588  psrmulr  19591  psrvscafval  19597  resspsrbas  19622  ressmplbas2  19662  opsrle  19682  opsrbaslem  19684  vr1val  19768  ressply1add  19806  ressply1mul  19807  ressply1vsca  19808  psrplusgpropd  19812  mplbaspropd  19813  psropprmul  19814  ply1baspropd  19819  ply1plusgpropd  19820  ply1sca2  19830  subrgvr1  19837  coe1mul2lem2  19844  ply1coe1eq  19874  zrhpropd  20069  znle  20090  frlmplusgval  20315  frlmvscafval  20317  mamudi  20417  mamudir  20418  matrcl  20426  oftpos  20467  mattpos1  20471  mdetfval  20601  mdetrlin  20617  mdetrsca  20618  mdetrsca2  20619  mdetrlin2  20622  mdetunilem5  20631  madufval  20652  madugsum  20658  idmatidpmat  20753  cpmidpmat  20889  cncmp  21407  2ndcsep  21474  llyeq  21485  nllyeq  21486  xkouni  21614  hmphindis  21812  xkocnv  21829  ptcmplem2  22068  snclseqg  22130  prdstmdd  22138  ustexsym  22230  ucnextcn  22319  metreslem  22378  comet  22529  nrmmetd  22590  nmpropd  22609  isngp3  22613  ngpds  22619  subgnm  22648  tngnm  22666  idnghm  22758  cnmetdval  22785  cnmpt2pc  22938  htpyco2  22989  phtpyco2  23000  clsocv  23259  rrxprds  23387  rrxnm  23389  ovolunlem1a  23475  voliunlem3  23531  ioombl1lem4  23540  uniioombllem4  23565  itg11  23670  itgeq1f  23750  itgeq2  23756  iblss2  23784  itgss  23790  itgeqa  23792  itgfsum  23805  itgsplit  23814  ditgeq1  23824  ditgeq2  23825  ditgeq3  23826  dvcmulf  23920  dvmptfsum  23950  dvcnvrelem2  23993  mdegfval  24034  mdegpropd  24056  deg1propd  24058  plyeq0  24179  coe11  24221  dgrlt  24234  dgradd2  24236  dgrmulc  24239  dvply1  24251  fta1lem  24274  pserulm  24388  rlimcnp2  24905  jensenlem1  24925  basellem5  25023  dchrbas  25172  dchrrcl  25177  dchrplusg  25184  dchrfi  25192  lgsdi  25271  lgseisenlem2  25313  lgsquadlem3  25319  dchrmusumlema  25394  rpvmasum2  25413  dchrisum0lema  25415  pntlemg  25499  colperpexlem2  25835  axlowdimlem13  26046  uhgrvtxedgiedgb  26243  uhgrvtxedgiedgbOLD  26244  nb3grprlem1  26496  crctcshlem2  26937  wpthswwlks2on  27100  clwlknf1oclwwlkn  27246  frgrncvvdeq  27482  avril1  27648  0vfval  27787  imsval  27866  imsdval  27867  bcseqi  28303  normpythi  28325  cm0  28794  fh1  28803  pjcji  28869  opsqrlem5  29329  pjsdi2i  29342  pjclem3  29382  pjci  29385  golem1  29456  iunrdx  29705  ofresid  29769  f1od2  29824  dp2eq1  29904  dp2eq2  29905  gsumvsca1  30105  gsumvsca2  30106  rhmopp  30142  resv1r  30160  fzto1st1  30175  crefeq  30235  xrge0mulc1cn  30310  qqhval2  30349  esumeq12dvaf  30416  esumeq2  30421  esumf1o  30435  esumfzf  30454  esumss  30457  esumpfinvalf  30461  ofceq  30482  carsgclctunlem1  30702  itgeq12dv  30711  ccatmulgnn0dir  30942  breprexpnat  31035  bnj956  31168  bnj1385  31224  bnj96  31256  bnj548  31288  bnj553  31289  bnj554  31290  bnj602  31306  bnj18eq1  31318  bnj1234  31402  bnj1296  31410  bnj1318  31414  bnj1442  31438  bnj1450  31439  cvmliftlem5  31592  cvmliftlem10  31597  cvmlift2lem9  31614  cvmliftphtlem  31620  mthmpps  31800  eqfunressuc  31980  rdgprc  32018  dfrdg2  32019  trpredeq1  32038  trpredeq2  32039  trpredeq3  32040  wsuceq123  32078  wlimeq12  32083  frecseq123  32096  nosupbnd2lem1  32180  altopthsn  32387  altxpeq1  32399  altxpeq2  32400  ee7.2aOLD  32775  bj-rabbida2  33221  bj-sngleq  33263  bj-tageq  33272  bj-projeq  33288  bj-projval  33292  bj-1upleq  33295  bj-pr1eq  33298  bj-pr2eq  33312  bj-evaleq  33333  csbpredg  33487  csbwrecsg  33488  csbrecsg  33489  csbrdgg  33490  csboprabg  33491  csbmpt22g  33492  finxpeq1  33537  finxpeq2  33538  csbfinxpg  33539  finxpreclem4  33545  cureq  33696  unceq  33697  uncov  33701  unccur  33703  finixpnum  33705  ptrest  33719  poimirlem3  33723  poimirlem9  33729  poimirlem15  33735  poimirlem16  33736  poimirlem26  33746  poimirlem27  33747  mbfposadd  33767  cnambfre  33768  iblabsnclem  33783  ftc1anclem1  33795  heiborlem4  33922  heiborlem6  33924  mpt2bi123f  34279  iineq12f  34281  mptbi12f  34283  eccnvepres  34360  uniqsALTV  34414  xrneq1  34450  xrneq2  34453  cosseq  34492  riotaclbgBAD  34731  toycom  34751  ldualvbase  34904  ldualfvadd  34906  ldualsca  34910  ldualsbase  34911  ldualsaddN  34912  ldualfvs  34914  ldual0  34925  ldual1  34926  ldualneg  34927  cdleme19f  36087  cdleme20m  36102  cdleme21k  36117  cdleme27b  36147  cdleme31so  36158  cdleme31sn  36159  cdleme31se  36161  cdleme31se2  36162  cdleme31sc  36163  cdleme31sde  36164  cdleme31fv  36169  cdleme40v  36248  cdleme43dN  36271  cdlemeg46ngfr  36297  ltrnco4  36518  tgrpbase  36525  tgrpopr  36526  erngbase  36580  erngfplus  36581  erngfmul  36584  erngbase-rN  36588  erngfplus-rN  36589  erngfmul-rN  36592  dvasca  36785  dvavbase  36792  dvafvadd  36793  dvafvsca  36795  tendocnv  36800  dvhsca  36861  dvhfplusr  36863  dvhvbase  36866  dvhfvadd  36870  dvhfvsca  36879  lcdvadd  37376  lcdsbase  37379  lcdsadd  37380  lcdvs  37382  lcd0  37387  lcd1  37388  lcdneg  37389  imaiinfv  37756  mapfzcons1  37780  rexrabdioph  37858  dnnumch1  38113  dnwech  38117  aomclem6  38128  pwssplit4  38158  pwfi2f1o  38165  mendplusgfval  38254  mendvscafval  38259  dssmapntrcls  38924  uzmptshftfval  39043  dropab1  39147  dropab2  39148  csbxpgOLD  39546  csbresgOLD  39548  csbrngOLD  39549  rabbida2  39806  rabbida3  39809  itgsinexplem1  40647  wallispi2lem2  40766  fourierdlem36  40837  etransclem4  40932  afveq12d  41720  aoveq123d  41765  aovfundmoveq  41768  aovnuoveq  41778  aovvoveq  41779  aovovn0oveq  41781  afv2eq12d  41802  fsumsplitsndif  41916  rngccofvalALTV  42553  ringccofvalALTV  42616  rhmsubclem2  42653  rhmsubcALTVlem2  42671  xpprsng  42676  setrecseq  42998  aacllem  43116
  Copyright terms: Public domain W3C validator