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

Theorem 3eqtr4g 2830
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 2817 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4g.3 . 2 𝐷 = 𝐵
53, 4syl6eqr 2823 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764
This theorem is referenced by:  rabbidva2  3336  rabeqf  3340  csbeq1  3685  csbeq2  3686  difeq1  3872  difeq2  3873  uneq2  3912  ineq2  3959  symdifeq1  3995  symdifeq2  3996  dfrab3ss  4053  csbprc  4124  csbeq2d  4135  csbnestgf  4140  disjssun  4178  ifeq1  4229  ifeq2  4230  pweq  4300  sneq  4326  csbsng  4380  csbprg  4381  rabsn  4392  preq1  4404  preq2  4405  tpeq1  4413  tpeq2  4414  tpeq3  4415  prprc1  4436  tpprceq3  4470  opeq1  4539  opeq2  4540  oteq1  4548  oteq2  4549  oteq3  4550  csbopg  4557  unieq  4582  csbuni  4602  inteq  4614  iineq1  4669  iineq2  4672  dfiin2g  4687  iinrab  4716  iinin1  4725  iinxprg  4735  iununi  4744  opabbid  4849  mpteq12f  4865  mpteq12d  4868  mpteq12df  4869  csbmpt12  5143  xpeq1  5263  xpeq2  5269  rneq  5489  reseq1  5528  reseq2  5529  resima2  5573  resindm  5585  resmpt  5590  resmptf  5592  imaeq1  5602  imaeq2  5603  mptcnv  5675  xpdisj1  5696  xpdisj2  5697  resdisj  5704  dmpropg  5750  rnpropg  5757  cores  5782  cores2  5792  xpco  5819  predeq123  5824  sspred  5831  suceq  5933  sucprc  5943  iotaeq  6002  iotabi  6003  fntpg  6089  imain  6114  f1oprswap  6321  fveq1  6331  fveq2  6332  fvres  6348  csbfv12  6372  fnimapr  6404  fvco2  6415  residpr  6552  fsnunfv  6597  fsnunres  6598  funiunfv  6649  fliftf  6708  isoini2  6732  riotaeqdv  6755  riotabidv  6756  riotauni  6760  riotabidva  6770  snriota  6784  oveq  6799  oveq1  6800  oveq2  6801  oprabbid  6855  mpt2eq123  6861  mpt2eq123dva  6863  mpt2eq3dva  6866  resmpt2  6905  ovres  6947  f1ocnvd  7031  ofeq  7046  ofreq  7047  fpar  7432  wrecseq123  7560  onovuni  7592  recseq  7623  tfr2a  7644  rdgeq1  7660  rdgeq2  7661  rdgsucmptf  7677  frsucmpt  7686  seqomeq12  7702  seqomsuc  7705  omopthi  7891  eceq1  7934  eceq2  7936  qseq1  7948  qseq2  7949  uniqs  7959  ecinxp  7974  qsinxp  7975  erovlem  7996  ecopovtrn  8003  ixpeq1  8073  supeq1  8507  supeq2  8510  supeq3  8511  supeq123d  8512  infeq1  8538  infeq2  8541  infeq3  8542  infeq123d  8543  infiso  8569  oieq1  8573  oieq2  8574  ordtypelem1  8579  inf3lemc  8687  wemapwe  8758  r1sucg  8796  r1limg  8798  rankprb  8878  karden  8922  djueq12  8931  cardiun  9008  acneq  9066  alephlim  9090  alephsuc  9091  alephfplem2  9128  infpssrlem2  9328  fin23lem34  9370  fin23lem35  9371  zorn2lem1  9520  zorn2lem7  9526  fpwwe2lem6  9659  fpwwe2lem13  9666  addpiord  9908  mulpiord  9909  addpqnq  9962  mulpqnq  9965  addassnq  9982  mulassnq  9983  distrnq  9985  lterpq  9994  ltexnq  9999  ltsrpr  10100  00sr  10122  recexsrlem  10126  mulgt0sr  10128  addcnsrec  10166  mulcnsrec  10167  negeq  10475  csbnegg  10480  negsubdi  10539  mulneg1  10668  negfi  11173  deceq1  11702  deceq1OLD  11703  deceq2  11704  deceq2OLD  11705  xnegeq  12243  fseq1p1m1  12621  om2uzrdg  12963  uzrdgsuci  12967  seqeq1  13011  seqeq2  13012  seqeq3  13013  seqfeq4  13057  seqof  13065  hashprg  13384  hashprgOLD  13385  hashtpg  13469  csbwrdg  13530  s1eq  13580  cats1co  13810  s2eqd  13817  s3eqd  13818  s4eqd  13819  s5eqd  13820  s6eqd  13821  s7eqd  13822  s8eqd  13823  xpcogend  13923  shftval  14022  limsupgle  14416  lo1eq  14507  rlimeq  14508  sumeq1  14627  sumeq2w  14630  sumeq2ii  14631  zsum  14657  sumss2  14665  fsumsplitsnun  14692  fsumsplitsnunOLD  14694  isumclim3  14698  fsumcom2  14713  incexclem  14775  incexc2  14777  isumshft  14778  prodeq1f  14845  prodeq2w  14849  prodeq2ii  14850  zprod  14874  fprodm1s  14907  fprodp1s  14908  fprodcom2  14921  iprodclim3  14937  ef0lem  15015  ruclem7  15171  sadcp1  15385  smupp1  15410  smueqlem  15420  algrp1  15495  dfphi2  15686  prmdiveq  15698  pceulem  15757  vdwlem6  15897  cshwsiun  16013  sloteq  16069  setsid  16121  elbasfv  16127  elbasov  16128  imastset  16390  imasvscaval  16406  xpscg  16426  isoval  16632  funcoppc  16742  fulloppc  16789  fuccofval  16826  natpropd  16843  catccofval  16957  xpchomfval  17027  xpccofval  17030  lubfval  17186  glbfval  17199  grpidpropd  17469  gsumpropd2lem  17481  frmdplusg  17599  grpinvpropd  17698  grpsubpropd  17728  grpsubpropd2  17729  mulgpropd  17792  oppgmnd  17991  symgplusg  18016  sylow1lem2  18221  sylow3lem1  18249  prds1  18822  pwsmgp  18826  opprring  18839  rngidpropd  18903  dvdsrpropd  18904  unitpropd  18905  invrpropd  18906  rhm1  18940  lmhmpropd  19286  lidlrsppropd  19445  lpival  19460  ressascl  19559  asclpropd  19561  aspval2  19562  psrbas  19593  psrplusg  19596  psrmulr  19599  psrvscafval  19605  resspsrbas  19630  ressmplbas2  19670  opsrle  19690  opsrbaslem  19692  opsrbaslemOLD  19693  vr1val  19777  ressply1add  19815  ressply1mul  19816  ressply1vsca  19817  psrplusgpropd  19821  mplbaspropd  19822  psropprmul  19823  ply1baspropd  19828  ply1plusgpropd  19829  ply1sca2  19839  subrgvr1  19846  coe1mul2lem2  19853  ply1coe1eq  19883  zrhpropd  20078  znle  20099  frlmplusgval  20324  frlmvscafval  20326  mamudi  20426  mamudir  20427  matrcl  20435  oftpos  20476  mattpos1  20480  mdetfval  20610  mdetrlin  20626  mdetrsca  20627  mdetrsca2  20628  mdetrlin2  20631  mdetunilem5  20640  madufval  20661  madugsum  20667  idmatidpmat  20762  cpmidpmat  20898  cncmp  21416  2ndcsep  21483  llyeq  21494  nllyeq  21495  xkouni  21623  hmphindis  21821  xkocnv  21838  ptcmplem2  22077  snclseqg  22139  prdstmdd  22147  ustexsym  22239  ucnextcn  22328  metreslem  22387  comet  22538  nrmmetd  22599  nmpropd  22618  isngp3  22622  ngpds  22628  subgnm  22657  tngnm  22675  idnghm  22767  cnmetdval  22794  cnmpt2pc  22947  htpyco2  22998  phtpyco2  23009  clsocv  23268  rrxprds  23396  rrxnm  23398  ovolunlem1a  23484  voliunlem3  23540  ioombl1lem4  23549  uniioombllem4  23574  itg11  23678  itgeq1f  23758  itgeq2  23764  iblss2  23792  itgss  23798  itgeqa  23800  itgfsum  23813  itgsplit  23822  ditgeq1  23832  ditgeq2  23833  ditgeq3  23834  dvcmulf  23928  dvmptfsum  23958  dvcnvrelem2  24001  mdegfval  24042  mdegpropd  24064  deg1propd  24066  plyeq0  24187  coe11  24229  dgrlt  24242  dgradd2  24244  dgrmulc  24247  dvply1  24259  fta1lem  24282  pserulm  24396  rlimcnp2  24914  jensenlem1  24934  basellem5  25032  dchrbas  25181  dchrrcl  25186  dchrplusg  25193  dchrfi  25201  lgsdi  25280  lgseisenlem2  25322  lgsquadlem3  25328  dchrmusumlema  25403  rpvmasum2  25422  dchrisum0lema  25424  pntlemg  25508  colperpexlem2  25844  axlowdimlem13  26055  uhgrvtxedgiedgb  26252  uhgrvtxedgiedgbOLD  26253  nb3grprlem1  26505  crctcshlem2  26946  wpthswwlks2on  27109  clwlknf1oclwwlkn  27255  frgrncvvdeq  27491  avril1  27661  0vfval  27801  imsval  27880  imsdval  27881  bcseqi  28317  normpythi  28339  cm0  28808  fh1  28817  pjcji  28883  opsqrlem5  29343  pjsdi2i  29356  pjclem3  29396  pjci  29399  golem1  29470  iunrdx  29720  ofresid  29784  f1od2  29839  dp2eq1  29920  dp2eq2  29921  gsumvsca1  30122  gsumvsca2  30123  rhmopp  30159  resv1r  30177  fzto1st1  30192  crefeq  30252  xrge0mulc1cn  30327  qqhval2  30366  esumeq12dvaf  30433  esumeq2  30438  esumf1o  30452  esumfzf  30471  esumss  30474  esumpfinvalf  30478  ofceq  30499  carsgclctunlem1  30719  itgeq12dv  30728  ccatmulgnn0dir  30959  breprexpnat  31052  bnj956  31185  bnj1385  31241  bnj96  31273  bnj548  31305  bnj553  31306  bnj554  31307  bnj602  31323  bnj18eq1  31335  bnj1234  31419  bnj1296  31427  bnj1318  31431  bnj1442  31455  bnj1450  31456  cvmliftlem5  31609  cvmliftlem10  31614  cvmlift2lem9  31631  cvmliftphtlem  31637  mthmpps  31817  eqfunressuc  31998  rdgprc  32036  dfrdg2  32037  trpredeq1  32056  trpredeq2  32057  trpredeq3  32058  wsuceq123  32096  wlimeq12  32101  frecseq123  32114  nosupbnd2lem1  32198  altopthsn  32405  altxpeq1  32417  altxpeq2  32418  ee7.2aOLD  32797  bj-rabbida2  33244  bj-sngleq  33286  bj-tageq  33295  bj-projeq  33311  bj-projval  33315  bj-1upleq  33318  bj-pr1eq  33321  bj-pr2eq  33335  bj-evaleq  33356  csbpredg  33509  csbwrecsg  33510  csbrecsg  33511  csbrdgg  33512  csboprabg  33513  csbmpt22g  33514  finxpeq1  33560  finxpeq2  33561  csbfinxpg  33562  finxpreclem4  33568  cureq  33718  unceq  33719  uncov  33723  unccur  33725  finixpnum  33727  ptrest  33741  poimirlem3  33745  poimirlem9  33751  poimirlem15  33757  poimirlem16  33758  poimirlem26  33768  poimirlem27  33769  mbfposadd  33789  cnambfre  33790  iblabsnclem  33805  ftc1anclem1  33817  heiborlem4  33945  heiborlem6  33947  mpt2bi123f  34303  iineq12f  34305  mptbi12f  34307  eccnvepres  34388  uniqsALTV  34444  xrneq1  34481  xrneq2  34484  cosseq  34523  riotaclbgBAD  34762  toycom  34782  ldualvbase  34935  ldualfvadd  34937  ldualsca  34941  ldualsbase  34942  ldualsaddN  34943  ldualfvs  34945  ldual0  34956  ldual1  34957  ldualneg  34958  cdleme19f  36117  cdleme20m  36132  cdleme21k  36147  cdleme27b  36177  cdleme31so  36188  cdleme31sn  36189  cdleme31se  36191  cdleme31se2  36192  cdleme31sc  36193  cdleme31sde  36194  cdleme31fv  36199  cdleme40v  36278  cdleme43dN  36301  cdlemeg46ngfr  36327  ltrnco4  36548  tgrpbase  36555  tgrpopr  36556  erngbase  36610  erngfplus  36611  erngfmul  36614  erngbase-rN  36618  erngfplus-rN  36619  erngfmul-rN  36622  dvasca  36815  dvavbase  36822  dvafvadd  36823  dvafvsca  36825  tendocnv  36831  dvhsca  36892  dvhfplusr  36894  dvhvbase  36897  dvhfvadd  36901  dvhfvsca  36910  lcdvadd  37407  lcdsbase  37410  lcdsadd  37411  lcdvs  37413  lcd0  37418  lcd1  37419  lcdneg  37420  imaiinfv  37782  mapfzcons1  37806  rexrabdioph  37884  dnnumch1  38140  dnwech  38144  aomclem6  38155  pwssplit4  38185  pwfi2f1o  38192  mendplusgfval  38281  mendvscafval  38286  dssmapntrcls  38952  uzmptshftfval  39071  dropab1  39176  dropab2  39177  csbxpgOLD  39576  csbresgOLD  39578  csbrngOLD  39579  rabbida2  39838  rabbida3  39841  itgsinexplem1  40687  wallispi2lem2  40806  fourierdlem36  40877  etransclem4  40972  afveq12d  41733  aoveq123d  41778  aovfundmoveq  41781  aovnuoveq  41791  aovvoveq  41792  aovovn0oveq  41794  fsumsplitsndif  41871  rngccofvalALTV  42515  ringccofvalALTV  42578  rhmsubclem2  42615  rhmsubcALTVlem2  42633  xpprsng  42638  setrecseq  42960  aacllem  43078
  Copyright terms: Public domain W3C validator