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

Theorem 3eqtr4g 2710
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 2697 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4g.3 . 2 𝐷 = 𝐵
53, 4syl6eqr 2703 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  rabbidva2  3217  rabeqf  3221  csbeq1  3569  csbeq2  3570  difeq1  3754  difeq2  3755  uneq2  3794  ineq2  3841  symdifeq1  3879  symdifeq2  3880  dfrab3ss  3938  csbprc  4013  csbeq2d  4024  csbnestgf  4029  disjssun  4069  ifeq1  4123  ifeq2  4124  pweq  4194  sneq  4220  csbsng  4275  csbprg  4276  rabsn  4288  preq1  4300  preq2  4301  tpeq1  4309  tpeq2  4310  tpeq3  4311  prprc1  4332  tpprceq3  4367  opeq1  4433  opeq2  4434  oteq1  4442  oteq2  4443  oteq3  4444  csbopg  4451  unieq  4476  csbuni  4498  inteq  4510  iineq1  4567  iineq2  4570  dfiin2g  4585  iinrab  4614  iinin1  4623  iinxprg  4633  iununi  4642  opabbid  4748  mpteq12f  4764  mpteq12d  4767  mpteq12df  4768  csbmpt12  5039  xpeq1  5157  xpeq2  5163  rneq  5383  reseq1  5422  reseq2  5423  resima2  5467  resindm  5479  resmpt  5484  resmptf  5486  imaeq1  5496  imaeq2  5497  mptcnv  5569  xpdisj1  5590  xpdisj2  5591  resdisj  5598  dmpropg  5644  rnpropg  5651  cores  5676  cores2  5686  xpco  5713  predeq123  5719  sspred  5726  suceq  5828  sucprc  5838  iotaeq  5897  iotabi  5898  fntpg  5986  imain  6012  f1oprswap  6218  fveq1  6228  fveq2  6229  fvres  6245  csbfv12  6269  fnimapr  6301  fvco2  6312  residpr  6449  fsnunfv  6494  fsnunres  6495  funiunfv  6546  fliftf  6605  isoini2  6629  riotaeqdv  6652  riotabidv  6653  riotauni  6657  riotabidva  6667  snriota  6681  oveq  6696  oveq1  6697  oveq2  6698  oprabbid  6750  mpt2eq123  6756  mpt2eq123dva  6758  mpt2eq3dva  6761  resmpt2  6800  ovres  6842  f1ocnvd  6926  ofeq  6941  ofreq  6942  fpar  7326  wrecseq123  7453  onovuni  7484  recseq  7515  tfr2a  7536  rdgeq1  7552  rdgeq2  7553  rdgsucmptf  7569  frsucmpt  7578  seqomeq12  7594  seqomsuc  7597  omopthi  7782  eceq1  7825  eceq2  7827  qseq1  7839  qseq2  7840  uniqs  7850  ecinxp  7865  qsinxp  7866  erovlem  7886  ecopovtrn  7893  ixpeq1  7961  supeq1  8392  supeq2  8395  supeq3  8396  supeq123d  8397  infeq1  8423  infeq2  8426  infeq3  8427  infeq123d  8428  infiso  8454  oieq1  8458  oieq2  8459  ordtypelem1  8464  inf3lemc  8561  wemapwe  8632  r1sucg  8670  r1limg  8672  rankprb  8752  karden  8796  cardiun  8846  acneq  8904  alephlim  8928  alephsuc  8929  alephfplem2  8966  infpssrlem2  9164  fin23lem34  9206  fin23lem35  9207  zorn2lem1  9356  zorn2lem7  9362  fpwwe2lem6  9495  fpwwe2lem13  9502  addpiord  9744  mulpiord  9745  addpqnq  9798  mulpqnq  9801  addassnq  9818  mulassnq  9819  distrnq  9821  lterpq  9830  ltexnq  9835  ltsrpr  9936  00sr  9958  recexsrlem  9962  mulgt0sr  9964  addcnsrec  10002  mulcnsrec  10003  negeq  10311  csbnegg  10316  negsubdi  10375  mulneg1  10504  negfi  11009  deceq1  11538  deceq1OLD  11539  deceq2  11540  deceq2OLD  11541  xnegeq  12076  fseq1p1m1  12452  om2uzrdg  12795  uzrdgsuci  12799  seqeq1  12844  seqeq2  12845  seqeq3  12846  seqfeq4  12890  seqof  12898  hashprg  13220  hashprgOLD  13221  hashmap  13260  hashtpg  13305  csbwrdg  13366  s1eq  13416  cats1co  13647  s2eqd  13654  s3eqd  13655  s4eqd  13656  s5eqd  13657  s6eqd  13658  s7eqd  13659  s8eqd  13660  xpcogend  13759  shftval  13858  limsupgle  14252  lo1eq  14343  rlimeq  14344  sumeq1  14463  sumeq2w  14466  sumeq2ii  14467  zsum  14493  sumss2  14501  fsumsplitsnun  14528  fsumsplitsnunOLD  14530  isumclim3  14534  fsumcom2  14549  fsumcom2OLD  14550  incexclem  14612  incexc2  14614  isumshft  14615  prodeq1f  14682  prodeq2w  14686  prodeq2ii  14687  zprod  14711  fprodm1s  14744  fprodp1s  14745  fprodcom2  14758  fprodcom2OLD  14759  iprodclim3  14775  ef0lem  14853  ruclem7  15009  sadcp1  15224  smupp1  15249  smueqlem  15259  algrp1  15334  dfphi2  15526  prmdiveq  15538  pceulem  15597  vdwlem6  15737  cshwsiun  15853  sloteq  15909  setsid  15961  elbasfv  15967  elbasov  15968  imastset  16229  imasvscaval  16245  xpscg  16265  isoval  16472  funcoppc  16582  fulloppc  16629  fuccofval  16666  natpropd  16683  catccofval  16797  xpchomfval  16866  xpccofval  16869  lubfval  17025  glbfval  17038  grpidpropd  17308  gsumpropd2lem  17320  frmdplusg  17438  grpinvpropd  17537  grpsubpropd  17567  grpsubpropd2  17568  mulgpropd  17631  oppgmnd  17830  symgplusg  17855  sylow1lem2  18060  sylow3lem1  18088  prds1  18660  pwsmgp  18664  opprring  18677  rngidpropd  18741  dvdsrpropd  18742  unitpropd  18743  invrpropd  18744  rhm1  18778  lmhmpropd  19121  lidlrsppropd  19278  lpival  19293  ressascl  19392  asclpropd  19394  aspval2  19395  psrbas  19426  psrplusg  19429  psrmulr  19432  psrvscafval  19438  resspsrbas  19463  ressmplbas2  19503  opsrle  19523  opsrbaslem  19525  opsrbaslemOLD  19526  vr1val  19610  ressply1add  19648  ressply1mul  19649  ressply1vsca  19650  psrplusgpropd  19654  mplbaspropd  19655  psropprmul  19656  ply1baspropd  19661  ply1plusgpropd  19662  ply1sca2  19672  subrgvr1  19679  coe1mul2lem2  19686  ply1coe1eq  19716  zrhpropd  19911  znle  19932  frlmplusgval  20155  frlmvscafval  20157  mamudi  20257  mamudir  20258  matrcl  20266  oftpos  20306  mattpos1  20310  mdetfval  20440  mdetrlin  20456  mdetrsca  20457  mdetrsca2  20458  mdetrlin2  20461  mdetunilem5  20470  madufval  20491  madugsum  20497  idmatidpmat  20590  cpmidpmat  20726  cncmp  21243  2ndcsep  21310  llyeq  21321  nllyeq  21322  xkouni  21450  hmphindis  21648  xkocnv  21665  ptcmplem2  21904  snclseqg  21966  prdstmdd  21974  ustexsym  22066  ucnextcn  22155  metreslem  22214  comet  22365  nrmmetd  22426  nmpropd  22445  isngp3  22449  ngpds  22455  subgnm  22484  tngnm  22502  idnghm  22594  cnmetdval  22621  cnmpt2pc  22774  htpyco2  22825  phtpyco2  22836  clsocv  23095  rrxprds  23223  rrxnm  23225  ovolunlem1a  23310  voliunlem3  23366  ioombl1lem4  23375  uniioombllem4  23400  itg11  23503  itgeq1f  23583  itgeq2  23589  iblss2  23617  itgss  23623  itgeqa  23625  itgfsum  23638  itgsplit  23647  ditgeq1  23657  ditgeq2  23658  ditgeq3  23659  dvcmulf  23753  dvmptfsum  23783  dvcnvrelem2  23826  mdegfval  23867  mdegpropd  23889  deg1propd  23891  plyeq0  24012  coe11  24054  dgrlt  24067  dgradd2  24069  dgrmulc  24072  dvply1  24084  fta1lem  24107  pserulm  24221  rlimcnp2  24738  jensenlem1  24758  basellem5  24856  dchrbas  25005  dchrrcl  25010  dchrplusg  25017  dchrfi  25025  lgsdi  25104  lgseisenlem2  25146  lgsquadlem3  25152  dchrmusumlema  25227  rpvmasum2  25246  dchrisum0lema  25248  pntlemg  25332  colperpexlem2  25668  axlowdimlem13  25879  uhgrvtxedgiedgb  26076  nb3grprlem1  26326  crctcshlem2  26766  wpthswwlks2on  26927  frgrncvvdeq  27289  avril1  27449  0vfval  27589  imsval  27668  imsdval  27669  bcseqi  28105  normpythi  28127  cm0  28596  fh1  28605  pjcji  28671  opsqrlem5  29131  pjsdi2i  29144  pjclem3  29184  pjci  29187  golem1  29258  iunrdx  29508  ofresid  29572  f1od2  29627  dp2eq1  29708  dp2eq2  29709  gsumvsca1  29910  gsumvsca2  29911  rhmopp  29947  resv1r  29965  fzto1st1  29980  crefeq  30040  xrge0mulc1cn  30115  qqhval2  30154  esumeq12dvaf  30221  esumeq2  30226  esumf1o  30240  esumfzf  30259  esumss  30262  esumpfinvalf  30266  ofceq  30287  carsgclctunlem1  30507  itgeq12dv  30516  ccatmulgnn0dir  30747  breprexpnat  30840  bnj956  30973  bnj1385  31029  bnj96  31061  bnj548  31093  bnj553  31094  bnj554  31095  bnj602  31111  bnj18eq1  31123  bnj1234  31207  bnj1296  31215  bnj1318  31219  bnj1442  31243  bnj1450  31244  cvmliftlem5  31397  cvmliftlem10  31402  cvmlift2lem9  31419  cvmliftphtlem  31425  mthmpps  31605  eqfunressuc  31786  rdgprc  31824  dfrdg2  31825  trpredeq1  31844  trpredeq2  31845  trpredeq3  31846  wsuceq123  31884  wlimeq12  31889  frecseq123  31902  nosupbnd2lem1  31986  altopthsn  32193  altxpeq1  32205  altxpeq2  32206  ee7.2aOLD  32585  bj-rabbida2  33038  bj-sngleq  33080  bj-tageq  33089  bj-projeq  33105  bj-projval  33109  bj-1upleq  33112  bj-pr1eq  33115  bj-pr2eq  33129  bj-evaleq  33149  csbpredg  33302  csbwrecsg  33303  csbrecsg  33304  csbrdgg  33305  csboprabg  33306  csbmpt22g  33307  finxpeq1  33353  finxpeq2  33354  csbfinxpg  33355  finxpreclem4  33361  cureq  33515  unceq  33516  uncov  33520  unccur  33522  finixpnum  33524  ptrest  33538  poimirlem3  33542  poimirlem9  33548  poimirlem15  33554  poimirlem16  33555  poimirlem26  33565  poimirlem27  33566  mbfposadd  33587  cnambfre  33588  iblabsnclem  33603  ftc1anclem1  33615  heiborlem4  33743  heiborlem6  33745  mpt2bi123f  34101  iineq12f  34103  mptbi12f  34105  eccnvepres  34186  uniqsALTV  34242  xrneq1  34279  xrneq2  34282  cosseq  34321  riotaclbgBAD  34558  toycom  34578  ldualvbase  34731  ldualfvadd  34733  ldualsca  34737  ldualsbase  34738  ldualsaddN  34739  ldualfvs  34741  ldual0  34752  ldual1  34753  ldualneg  34754  cdleme19f  35913  cdleme20m  35928  cdleme21k  35943  cdleme27b  35973  cdleme31so  35984  cdleme31sn  35985  cdleme31se  35987  cdleme31se2  35988  cdleme31sc  35989  cdleme31sde  35990  cdleme31fv  35995  cdleme40v  36074  cdleme43dN  36097  cdlemeg46ngfr  36123  ltrnco4  36344  tgrpbase  36351  tgrpopr  36352  erngbase  36406  erngfplus  36407  erngfmul  36410  erngbase-rN  36414  erngfplus-rN  36415  erngfmul-rN  36418  dvasca  36611  dvavbase  36618  dvafvadd  36619  dvafvsca  36621  tendocnv  36627  dvhsca  36688  dvhfplusr  36690  dvhvbase  36693  dvhfvadd  36697  dvhfvsca  36706  lcdvadd  37203  lcdsbase  37206  lcdsadd  37207  lcdvs  37209  lcd0  37214  lcd1  37215  lcdneg  37216  imaiinfv  37573  mapfzcons1  37597  rexrabdioph  37675  dnnumch1  37931  dnwech  37935  aomclem6  37946  pwssplit4  37976  pwfi2f1o  37983  mendplusgfval  38072  mendvscafval  38077  dssmapntrcls  38743  uzmptshftfval  38862  dropab1  38968  dropab2  38969  csbxpgOLD  39368  csbresgOLD  39370  csbrngOLD  39371  rabbida2  39631  rabbida3  39634  itgsinexplem1  40487  wallispi2lem2  40607  fourierdlem36  40678  etransclem4  40773  afveq12d  41534  aoveq123d  41579  aovfundmoveq  41582  aovnuoveq  41592  aovvoveq  41593  aovovn0oveq  41595  fsumsplitsndif  41668  rngccofvalALTV  42312  ringccofvalALTV  42375  rhmsubclem2  42412  rhmsubcALTVlem2  42430  xpprsng  42435  setrecseq  42757  aacllem  42875
  Copyright terms: Public domain W3C validator