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

Theorem 3eqtr4g 2493
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3eqtr4g.1  |-  ( ph  ->  A  =  B )
3eqtr4g.2  |-  C  =  A
3eqtr4g.3  |-  D  =  B
Assertion
Ref Expression
3eqtr4g  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr4g
StepHypRef Expression
1 3eqtr4g.2 . . 3  |-  C  =  A
2 3eqtr4g.1 . . 3  |-  ( ph  ->  A  =  B )
31, 2syl5eq 2480 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4g.3 . 2  |-  D  =  B
53, 4syl6eqr 2486 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  rabeqf  2949  csbeq1  3254  csbeq2d  3275  csbnestgf  3299  difeq1  3458  difeq2  3459  uneq2  3495  ineq2  3536  dfrab3ss  3619  ifeq1  3743  ifeq2  3744  pweq  3802  sneq  3825  csbsng  3867  rabsn  3873  preq1  3883  preq2  3884  tpeq1  3892  tpeq2  3893  tpeq3  3894  prprc1  3914  opeq1  3984  opeq2  3985  oteq1  3993  oteq2  3994  oteq3  3995  csbunig  4023  unieq  4024  inteq  4053  iineq1  4107  iineq2  4110  dfiin2g  4124  iinrab  4153  iinin1  4162  iinxprg  4168  iununi  4175  opabbid  4270  mpteq12f  4285  suceq  4646  xpeq1  4892  xpeq2  4893  csbxpg  4905  rneq  5095  csbrng  5114  reseq1  5140  reseq2  5141  csbresg  5149  resmpt  5191  imaeq1  5198  imaeq2  5199  csbima12gALT  5214  dmpropg  5343  cores  5373  cores2  5382  xpco  5414  iotaeq  5426  iotabi  5427  fntpg  5506  imain  5529  f1oprswap  5717  fveq1  5727  fveq2  5728  csbfv12g  5738  csbfv12gALT  5739  fvres  5745  fnimapr  5787  fvco2  5798  fsnunfv  5933  fsnunres  5934  funiunfv  5995  fliftf  6037  isoini2  6059  oveq  6087  oveq1  6088  oveq2  6089  oprabbid  6127  mpt2eq123  6133  mpt2eq123dva  6135  mpt2eq3dva  6138  resmpt2  6168  ovres  6213  f1ocnvd  6293  ofeq  6307  ofreq  6308  fpar  6450  riotaeqdv  6550  riotabidv  6551  riotabidva  6566  riotaund  6586  onovuni  6604  recseq  6634  tfr2a  6656  rdgeq1  6669  rdgeq2  6670  rdgsucmptf  6686  frsucmpt  6695  seqomeq12  6711  seqomsuc  6714  abianfplem  6715  omopthi  6900  eceq1  6941  eceq2  6942  qseq1  6954  qseq2  6955  uniqs  6964  ecinxp  6979  qsinxp  6980  erovlem  7000  ecopovtrn  7007  ixpeq1  7073  supeq1  7450  supeq2  7453  supeq3  7454  supeq123d  7455  oieq1  7481  oieq2  7482  ordtypelem1  7487  inf3lemc  7581  cantnfreslem  7631  wemapwe  7654  r1sucg  7695  r1limg  7697  rankprb  7777  karden  7819  cardiun  7869  acneq  7924  alephlim  7948  alephsuc  7949  alephfplem2  7986  dfac2a  8010  infpssrlem2  8184  fin23lem34  8226  fin23lem35  8227  zorn2lem1  8376  zorn2lem7  8382  fpwwe2lem6  8510  fpwwe2lem13  8517  addpiord  8761  mulpiord  8762  addpqnq  8815  mulpqnq  8818  addassnq  8835  mulassnq  8836  distrnq  8838  lterpq  8847  ltexnq  8852  ltsrpr  8952  00sr  8974  recexsrlem  8978  mulgt0sr  8980  addcnsrec  9018  mulcnsrec  9019  negeq  9298  csbnegg  9303  negsubdi  9357  mulneg1  9470  deceq1  10385  deceq2  10386  xnegeq  10793  fseq1p1m1  11122  om2uzrdg  11296  uzrdgsuci  11300  seqeq1  11326  seqeq2  11327  seqeq3  11328  seqfeq4  11372  seqof  11380  hashprg  11666  hashtpg  11691  hashmap  11698  hashbclem  11701  s1eq  11753  cats1co  11820  s2eqd  11826  s3eqd  11827  s4eqd  11828  s5eqd  11829  s6eqd  11830  s7eqd  11831  s8eqd  11832  shftval  11889  limsupgle  12271  lo1eq  12362  rlimeq  12363  sumeq1f  12482  sumeq2w  12486  sumeq2ii  12487  zsum  12512  sumss2  12520  isumclim3  12543  fsumcom2  12558  fsumrev  12562  fsumshft  12563  incexclem  12616  incexc2  12618  isumshft  12619  ef0lem  12681  ruclem7  12835  sadcp1  12967  smupp1  12992  smueqlem  13002  algrp1  13065  dfphi2  13163  prmdiveq  13175  pceulem  13219  vdwlem6  13354  setsid  13508  elbasfv  13512  elbasov  13513  imastset  13747  imasvscaval  13763  xpscg  13783  isoval  13990  funcoppc  14072  fulloppc  14119  fuccofval  14156  natpropd  14173  catccofval  14255  xpchomfval  14276  xpccofval  14279  grpidpropd  14722  frmdplusg  14799  grpinvpropd  14866  grpsubpropd  14889  grpsubpropd2  14890  mulgpropd  14923  symgplusg  15099  oppgmnd  15150  sylow1lem2  15233  sylow3lem1  15261  prds1  15720  pwsmgp  15724  opprrng  15736  rngidpropd  15800  dvdsrpropd  15801  unitpropd  15802  invrpropd  15803  rhm1  15831  lmhmpropd  16145  lidlrsppropd  16301  lpival  16316  rrgsupp  16351  ressascl  16402  asclpropd  16404  aspval2  16405  psrbas  16443  psrplusg  16445  psrmulr  16448  psrvscafval  16454  resspsrbas  16478  ressmplbas2  16518  opsrle  16536  opsrbaslem  16538  mplrcl  16550  vr1val  16590  ressply1add  16624  ressply1mul  16625  ressply1vsca  16626  psrplusgpropd  16629  mplbaspropd  16630  strov2rcl  16631  psropprmul  16632  ply1baspropd  16637  ply1plusgpropd  16638  ply1sca2  16648  subrgvr1  16654  coe1mul2lem2  16661  zrhpropd  16796  znle  16817  cncmp  17455  2ndcsep  17522  llyeq  17533  nllyeq  17534  xkouni  17631  hmphindis  17829  pt1hmeo  17838  xkocnv  17846  ptcmplem2  18084  snclseqg  18145  prdstmdd  18153  ustexsym  18245  ucnextcn  18334  metreslem  18392  comet  18543  nrmmetd  18622  nmpropd  18641  isngp3  18645  ngpds  18650  subgnm  18674  tngnm  18692  idnghm  18777  cnmetdval  18805  cnmpt2pc  18953  htpyco2  19004  phtpyco2  19015  clsocv  19204  ovolunlem1a  19392  voliunlem3  19446  ioombl1lem4  19455  uniioombllem4  19478  itg11  19583  itgeq1f  19663  itgeq2  19669  iblss2  19697  itgss  19703  itgeqa  19705  itgfsum  19718  itgsplit  19727  ditgeq1  19735  ditgeq2  19736  ditgeq3  19737  dvcmulf  19831  dvmptfsum  19859  dvcnvrelem2  19902  mdegfval  19985  mdegpropd  20007  deg1propd  20009  plyeq0  20130  coe11  20171  dgrlt  20184  dgradd2  20186  dgrmulc  20189  dvply1  20201  fta1lem  20224  pserulm  20338  rlimcnp2  20805  jensenlem1  20825  basellem5  20867  dchrbas  21019  dchrrcl  21024  dchrplusg  21031  dchrfi  21039  lgsdi  21116  lgseisenlem2  21134  lgsquadlem3  21140  dchrmusumlema  21187  rpvmasum2  21206  dchrisum0lema  21208  pntlemg  21292  isusgra0  21376  nbgraf1olem5  21455  nb3graprlem1  21460  constr2spthlem1  21594  constr3pthlem1  21642  constr3pthlem2  21643  avril1  21757  0vfval  22085  imsval  22177  imsdval  22178  bcseqi  22622  normpythi  22644  cm0  23111  fh1  23120  pjcji  23186  opsqrlem5  23647  pjsdi2i  23660  pjclem3  23700  pjci  23703  golem1  23774  rabbidva2  23986  iunrdx  24014  rnpropg  24035  mptcnv  24045  ofresid  24055  resmptf  24071  gsumpropd2lem  24220  rhmopp  24257  xrge0mulc1cn  24327  qqhval2  24366  esumeq12dvaf  24428  esumeq2  24433  esumf1o  24445  esumfzf  24459  esumss  24462  esumpfinvalf  24466  ofceq  24480  itgeq12dv  24641  cvmliftlem5  24976  cvmliftlem10  24981  cvmlift2lem9  24998  cvmliftphtlem  25004  prodeq1f  25234  prodeq2w  25238  prodeq2ii  25239  zprod  25263  fprodm1s  25293  fprodp1s  25294  fprodshft  25300  fprodrev  25301  fprodcom2  25308  iprodclim3  25313  mpteq12d  25396  rdgprc  25422  dfrdg2  25423  predeq123  25440  trpredeq1  25498  trpredeq2  25499  trpredeq3  25500  wrecseq123  25532  wsuceq123  25565  wlimeq12  25570  symdifeq1  25665  symdifeq2  25666  altopthsn  25806  altxpeq1  25818  altxpeq2  25819  axlowdimlem13  25893  ee7.2aOLD  26211  mbfposadd  26254  cnambfre  26255  iblabsnclem  26268  ftc1anclem1  26280  heiborlem4  26523  heiborlem6  26525  imaiinfv  26740  mapfzcons1  26773  rexrabdioph  26854  dnnumch1  27119  dnwech  27123  aomclem6  27134  pwssplit4  27168  frlmplusgval  27206  frlmvscafval  27207  pwfi2f1o  27237  mamudi  27438  mamudir  27439  matrcl  27443  mdetfval  27464  mendplusgfval  27470  mendvscafval  27475  dropab1  27626  dropab2  27627  itgsinexplem1  27724  wallispi2lem2  27797  csbdmg  27958  afveq12d  27973  aoveq123d  28018  aovfundmoveq  28021  aovnuoveq  28031  aovvoveq  28032  aovovn0oveq  28034  resisresindm  28074  cshwsiun  28286  bnj956  29147  bnj1385  29204  bnj96  29236  bnj548  29268  bnj553  29269  bnj554  29270  bnj602  29286  bnj18eq1  29298  bnj1234  29382  bnj1296  29390  bnj1318  29394  bnj1442  29418  bnj1450  29419  toycom  29770  ldualvbase  29924  ldualfvadd  29926  ldualsca  29930  ldualsbase  29931  ldualsaddN  29932  ldualfvs  29934  ldual0  29945  ldual1  29946  ldualneg  29947  cdleme19f  31105  cdleme20m  31120  cdleme21k  31135  cdleme27b  31165  cdleme31so  31176  cdleme31sn  31177  cdleme31se  31179  cdleme31se2  31180  cdleme31sc  31181  cdleme31sde  31182  cdleme31fv  31187  cdleme40v  31266  cdleme43dN  31289  cdlemeg46ngfr  31315  ltrnco4  31536  tgrpbase  31543  tgrpopr  31544  erngbase  31598  erngfplus  31599  erngfmul  31602  erngbase-rN  31606  erngfplus-rN  31607  erngfmul-rN  31610  dvasca  31803  dvavbase  31810  dvafvadd  31811  dvafvsca  31813  tendocnv  31819  dvhsca  31880  dvhfplusr  31882  dvhvbase  31885  dvhfvadd  31889  dvhfvsca  31898  lcdvadd  32395  lcdsbase  32398  lcdsadd  32399  lcdvs  32401  lcd0  32406  lcd1  32407  lcdneg  32408  mapdvalc  32427  mapdval4N  32430
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator