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

Theorem 3eqtr4g 2469
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 2456 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4g.3 . 2  |-  D  =  B
53, 4syl6eqr 2462 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  rabeqf  2917  csbeq1  3222  csbeq2d  3243  csbnestgf  3267  difeq1  3426  difeq2  3427  uneq2  3463  ineq2  3504  dfrab3ss  3587  ifeq1  3711  ifeq2  3712  pweq  3770  sneq  3793  csbsng  3835  rabsn  3841  preq1  3851  preq2  3852  tpeq1  3860  tpeq2  3861  tpeq3  3862  prprc1  3882  opeq1  3952  opeq2  3953  oteq1  3961  oteq2  3962  oteq3  3963  csbunig  3991  unieq  3992  inteq  4021  iineq1  4075  iineq2  4078  dfiin2g  4092  iinrab  4121  iinin1  4130  iinxprg  4136  iununi  4143  opabbid  4238  mpteq12f  4253  suceq  4614  xpeq1  4859  xpeq2  4860  csbxpg  4872  rneq  5062  csbrng  5081  reseq1  5107  reseq2  5108  csbresg  5116  resmpt  5158  imaeq1  5165  imaeq2  5166  csbima12gALT  5181  dmpropg  5310  cores  5340  cores2  5349  xpco  5381  iotaeq  5393  iotabi  5394  fntpg  5473  imain  5496  f1oprswap  5684  fveq1  5694  fveq2  5695  csbfv12g  5705  csbfv12gALT  5706  fvres  5712  fnimapr  5754  fvco2  5765  fsnunfv  5900  fsnunres  5901  funiunfv  5962  fliftf  6004  isoini2  6026  oveq  6054  oveq1  6055  oveq2  6056  oprabbid  6094  mpt2eq123  6100  mpt2eq123dva  6102  mpt2eq3dva  6105  resmpt2  6135  ovres  6180  f1ocnvd  6260  ofeq  6274  ofreq  6275  fpar  6417  riotaeqdv  6517  riotabidv  6518  riotabidva  6533  riotaund  6553  onovuni  6571  recseq  6601  tfr2a  6623  rdgeq1  6636  rdgeq2  6637  rdgsucmptf  6653  frsucmpt  6662  seqomeq12  6678  seqomsuc  6681  abianfplem  6682  omopthi  6867  eceq1  6908  eceq2  6909  qseq1  6921  qseq2  6922  uniqs  6931  ecinxp  6946  qsinxp  6947  erovlem  6967  ecopovtrn  6974  ixpeq1  7040  supeq1  7416  supeq2  7419  oieq1  7445  oieq2  7446  ordtypelem1  7451  inf3lemc  7545  cantnfreslem  7595  wemapwe  7618  r1sucg  7659  r1limg  7661  rankprb  7741  karden  7783  cardiun  7833  acneq  7888  alephlim  7912  alephsuc  7913  alephfplem2  7950  dfac2a  7974  infpssrlem2  8148  fin23lem34  8190  fin23lem35  8191  zorn2lem1  8340  zorn2lem7  8346  fpwwe2lem6  8474  fpwwe2lem13  8481  addpiord  8725  mulpiord  8726  addpqnq  8779  mulpqnq  8782  addassnq  8799  mulassnq  8800  distrnq  8802  lterpq  8811  ltexnq  8816  ltsrpr  8916  00sr  8938  recexsrlem  8942  mulgt0sr  8944  addcnsrec  8982  mulcnsrec  8983  negeq  9262  csbnegg  9267  negsubdi  9321  mulneg1  9434  deceq1  10349  deceq2  10350  xnegeq  10757  fseq1p1m1  11085  om2uzrdg  11259  uzrdgsuci  11263  seqeq1  11289  seqeq2  11290  seqeq3  11291  seqfeq4  11335  seqof  11343  hashprg  11629  hashtpg  11654  hashmap  11661  hashbclem  11664  s1eq  11716  cats1co  11783  s2eqd  11789  s3eqd  11790  s4eqd  11791  s5eqd  11792  s6eqd  11793  s7eqd  11794  s8eqd  11795  shftval  11852  limsupgle  12234  lo1eq  12325  rlimeq  12326  sumeq1f  12445  sumeq2w  12449  sumeq2ii  12450  zsum  12475  sumss2  12483  isumclim3  12506  fsumcom2  12521  fsumrev  12525  fsumshft  12526  incexclem  12579  incexc2  12581  isumshft  12582  ef0lem  12644  ruclem7  12798  sadcp1  12930  smupp1  12955  smueqlem  12965  algrp1  13028  dfphi2  13126  prmdiveq  13138  pceulem  13182  vdwlem6  13317  setsid  13471  elbasfv  13475  elbasov  13476  imastset  13710  imasvscaval  13726  xpscg  13746  isoval  13953  funcoppc  14035  fulloppc  14082  fuccofval  14119  natpropd  14136  catccofval  14218  xpchomfval  14239  xpccofval  14242  grpidpropd  14685  frmdplusg  14762  grpinvpropd  14829  grpsubpropd  14852  grpsubpropd2  14853  mulgpropd  14886  symgplusg  15062  oppgmnd  15113  sylow1lem2  15196  sylow3lem1  15224  prds1  15683  pwsmgp  15687  opprrng  15699  rngidpropd  15763  dvdsrpropd  15764  unitpropd  15765  invrpropd  15766  rhm1  15794  lmhmpropd  16108  lidlrsppropd  16264  lpival  16279  rrgsupp  16314  ressascl  16365  asclpropd  16367  aspval2  16368  psrbas  16406  psrplusg  16408  psrmulr  16411  psrvscafval  16417  resspsrbas  16441  ressmplbas2  16481  opsrle  16499  opsrbaslem  16501  mplrcl  16513  vr1val  16553  ressply1add  16587  ressply1mul  16588  ressply1vsca  16589  psrplusgpropd  16592  mplbaspropd  16593  strov2rcl  16594  psropprmul  16595  ply1baspropd  16600  ply1plusgpropd  16601  ply1sca2  16611  subrgvr1  16617  coe1mul2lem2  16624  zrhpropd  16759  znle  16780  cncmp  17417  2ndcsep  17483  llyeq  17494  nllyeq  17495  xkouni  17592  hmphindis  17790  pt1hmeo  17799  xkocnv  17807  ptcmplem2  18045  snclseqg  18106  prdstmdd  18114  ustexsym  18206  ucnextcn  18295  metreslem  18353  comet  18504  nrmmetd  18583  nmpropd  18602  isngp3  18606  ngpds  18611  subgnm  18635  tngnm  18653  idnghm  18738  cnmetdval  18766  cnmpt2pc  18914  htpyco2  18965  phtpyco2  18976  clsocv  19165  ovolunlem1a  19353  voliunlem3  19407  ioombl1lem4  19416  uniioombllem4  19439  itg11  19544  itgeq1f  19624  itgeq2  19630  iblss2  19658  itgss  19664  itgeqa  19666  itgfsum  19679  itgsplit  19688  ditgeq1  19696  ditgeq2  19697  ditgeq3  19698  dvcmulf  19792  dvmptfsum  19820  dvcnvrelem2  19863  mdegfval  19946  mdegpropd  19968  deg1propd  19970  plyeq0  20091  coe11  20132  dgrlt  20145  dgradd2  20147  dgrmulc  20150  dvply1  20162  fta1lem  20185  pserulm  20299  rlimcnp2  20766  jensenlem1  20786  basellem5  20828  dchrbas  20980  dchrrcl  20985  dchrplusg  20992  dchrfi  21000  lgsdi  21077  lgseisenlem2  21095  lgsquadlem3  21101  dchrmusumlema  21148  rpvmasum2  21167  dchrisum0lema  21169  pntlemg  21253  isusgra0  21337  nbgraf1olem5  21416  nb3graprlem1  21421  constr2spthlem1  21555  constr3pthlem1  21603  constr3pthlem2  21604  avril1  21718  0vfval  22046  imsval  22138  imsdval  22139  bcseqi  22583  normpythi  22605  cm0  23072  fh1  23081  pjcji  23147  opsqrlem5  23608  pjsdi2i  23621  pjclem3  23661  pjci  23664  golem1  23735  rabbidva2  23947  iunrdx  23975  rnpropg  23996  mptcnv  24006  ofresid  24016  resmptf  24032  gsumpropd2lem  24181  rhmopp  24218  xrge0mulc1cn  24288  qqhval2  24327  esumeq12dvaf  24389  esumeq2  24394  esumf1o  24406  esumfzf  24420  esumss  24423  esumpfinvalf  24427  ofceq  24441  itgeq12dv  24602  cvmliftlem5  24937  cvmliftlem10  24942  cvmlift2lem9  24959  cvmliftphtlem  24965  prodeq1f  25195  prodeq2w  25199  prodeq2ii  25200  zprod  25224  fprodm1s  25254  fprodp1s  25255  fprodshft  25261  fprodrev  25262  fprodcom2  25269  iprodclim3  25274  mpteq12d  25350  rdgprc  25373  dfrdg2  25374  predeq1  25391  predeq2  25392  predeq3  25393  trpredeq1  25445  trpredeq2  25446  trpredeq3  25447  symdifeq1  25586  symdifeq2  25587  altopthsn  25718  altxpeq1  25730  altxpeq2  25731  axlowdimlem13  25805  ee7.2aOLD  26123  mbfposadd  26161  cnambfre  26162  iblabsnclem  26175  heiborlem4  26421  heiborlem6  26423  imaiinfv  26638  mapfzcons1  26671  rexrabdioph  26752  dnnumch1  27017  dnwech  27021  aomclem6  27032  supeq123d  27034  pwssplit4  27067  frlmplusgval  27105  frlmvscafval  27106  pwfi2f1o  27136  mamudi  27337  mamudir  27338  matrcl  27342  mdetfval  27363  mendplusgfval  27369  mendvscafval  27374  dropab1  27525  dropab2  27526  itgsinexplem1  27623  wallispi2lem2  27696  csbdmg  27857  afveq12d  27872  aoveq123d  27917  aovfundmoveq  27920  aovnuoveq  27930  aovvoveq  27931  aovovn0oveq  27933  resisresindm  27965  bnj956  28865  bnj1385  28922  bnj96  28954  bnj548  28986  bnj553  28987  bnj554  28988  bnj602  29004  bnj18eq1  29016  bnj1234  29100  bnj1296  29108  bnj1318  29112  bnj1442  29136  bnj1450  29137  toycom  29467  ldualvbase  29621  ldualfvadd  29623  ldualsca  29627  ldualsbase  29628  ldualsaddN  29629  ldualfvs  29631  ldual0  29642  ldual1  29643  ldualneg  29644  cdleme19f  30802  cdleme20m  30817  cdleme21k  30832  cdleme27b  30862  cdleme31so  30873  cdleme31sn  30874  cdleme31se  30876  cdleme31se2  30877  cdleme31sc  30878  cdleme31sde  30879  cdleme31fv  30884  cdleme40v  30963  cdleme43dN  30986  cdlemeg46ngfr  31012  ltrnco4  31233  tgrpbase  31240  tgrpopr  31241  erngbase  31295  erngfplus  31296  erngfmul  31299  erngbase-rN  31303  erngfplus-rN  31304  erngfmul-rN  31307  dvasca  31500  dvavbase  31507  dvafvadd  31508  dvafvsca  31510  tendocnv  31516  dvhsca  31577  dvhfplusr  31579  dvhvbase  31582  dvhfvadd  31586  dvhfvsca  31595  lcdvadd  32092  lcdsbase  32095  lcdsadd  32096  lcdvs  32098  lcd0  32103  lcd1  32104  lcdneg  32105  mapdvalc  32124  mapdval4N  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2405
  Copyright terms: Public domain W3C validator