Theorem 3eqtr4g 2509

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 21-Jun-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

Step	Hyp	Ref	Expression
1		3eqtr4g.2	. . 3 |- C = A
2		3eqtr4g.1	. . 3 |- ( ph -> A = B )
3	1, 2	syl5eq 2496	. 2 |- ( ph -> C = B )
4		3eqtr4g.3	. 2 |- D = B
5	3, 4	syl6eqr 2502	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-cleq 2435

This theorem is referenced by:  rabbidva2  3085  rabeqf  3088  csbeq1  3423  csbeq2  3424  difeq1  3600  difeq2  3601  uneq2  3637  ineq2  3679  dfrab3ss  3761  csbeq2d  3820  csbnestgf  3826  ifeq1  3930  ifeq2  3931  pweq  4000  sneq  4024  csbsng  4073  csbprg  4074  rabsn  4082  preq1  4094  preq2  4095  tpeq1  4103  tpeq2  4104  tpeq3  4105  prprc1  4125  opeq1  4202  opeq2  4203  oteq1  4211  oteq2  4212  oteq3  4213  unieq  4242  csbuni  4262  csbunigOLD  4263  inteq  4274  iineq1  4330  iineq2  4333  dfiin2g  4348  iinrab  4377  iinin1  4386  iinxprg  4393  iununi  4400  opabbid  4499  mpteq12f  4513  csbmpt12  4771  suceq  4933  xpeq1  5003  xpeq2  5004  csbxpgOLD  5072  rneq  5218  reseq1  5257  reseq2  5258  csbresgOLD  5267  resmpt  5313  imaeq1  5322  imaeq2  5323  mptcnv  5398  csbrngOLD  5459  dmpropg  5471  rnpropg  5478  cores  5500  cores2  5510  xpco  5537  iotaeq  5549  iotabi  5550  fntpg  5633  imain  5654  f1oprswap  5845  fveq1  5855  fveq2  5856  fvres  5870  csbfv12  5891  csbfv12gOLD  5892  fnimapr  5922  fvco2  5933  residpr  6060  fsnunfv  6096  fsnunres  6097  funiunfv  6145  fliftf  6198  isoini2  6220  riotaeqdv  6243  riotabidv  6244  riotauni  6248  riotabidva  6259  snriota  6272  oveq  6287  oveq1  6288  oveq2  6289  oprabbid  6335  mpt2eq123  6341  mpt2eq123dva  6343  mpt2eq3dva  6346  resmpt2  6385  ovres  6427  f1ocnvd  6509  ofeq  6527  ofreq  6528  fpar  6889  onovuni  7015  recseq  7045  tfr2a  7066  rdgeq1  7079  rdgeq2  7080  rdgsucmptf  7096  frsucmpt  7105  seqomeq12  7121  seqomsuc  7124  omopthi  7308  eceq1  7349  eceq2  7351  qseq1  7363  qseq2  7364  uniqs  7373  ecinxp  7388  qsinxp  7389  erovlem  7409  ecopovtrn  7416  ixpeq1  7482  supeq1  7907  supeq2  7910  supeq3  7911  supeq123d  7912  oieq1  7940  oieq2  7941  ordtypelem1  7946  inf3lemc  8046  wemapwe  8142  wemapweOLD  8143  r1sucg  8190  r1limg  8192  rankprb  8272  karden  8316  cardiun  8366  acneq  8427  alephlim  8451  alephsuc  8452  alephfplem2  8489  infpssrlem2  8687  fin23lem34  8729  fin23lem35  8730  zorn2lem1  8879  zorn2lem7  8885  fpwwe2lem6  9016  fpwwe2lem13  9023  addpiord  9265  mulpiord  9266  addpqnq  9319  mulpqnq  9322  addassnq  9339  mulassnq  9340  distrnq  9342  lterpq  9351  ltexnq  9356  ltsrpr  9457  00sr  9479  recexsrlem  9483  mulgt0sr  9485  addcnsrec  9523  mulcnsrec  9524  negeq  9817  csbnegg  9822  negsubdi  9880  mulneg1  10000  deceq1  10988  deceq2  10989  xnegeq  11416  fseq1p1m1  11762  om2uzrdg  12048  uzrdgsuci  12052  seqeq1  12091  seqeq2  12092  seqeq3  12093  seqfeq4  12137  seqof  12145  hashprg  12441  hashmap  12474  hashtpg  12504  csbwrdg  12551  s1eq  12593  cats1co  12802  s2eqd  12808  s3eqd  12809  s4eqd  12810  s5eqd  12811  s6eqd  12812  s7eqd  12813  s8eqd  12814  shftval  12888  limsupgle  13281  lo1eq  13372  rlimeq  13373  sumeq1  13492  sumeq2w  13495  sumeq2ii  13496  zsum  13521  sumss2  13529  fsumsplitsnun  13551  isumclim3  13555  fsumcom2  13570  incexclem  13629  incexc2  13631  isumshft  13632  prodeq1f  13696  prodeq2w  13700  prodeq2ii  13701  zprod  13725  fprodm1s  13755  fprodp1s  13756  fprodcom2  13769  iprodclim3  13774  ef0lem  13795  ruclem7  13950  sadcp1  14086  smupp1  14111  smueqlem  14121  algrp1  14184  dfphi2  14285  prmdiveq  14297  pceulem  14350  vdwlem6  14485  cshwsiun  14565  setsid  14654  elbasfv  14660  elbasov  14661  imastset  14900  imasvscaval  14916  xpscg  14936  isoval  15140  funcoppc  15222  fulloppc  15269  fuccofval  15306  natpropd  15323  catccofval  15405  xpchomfval  15426  xpccofval  15429  lubfval  15586  glbfval  15599  grpidpropd  15866  gsumpropd2lem  15878  frmdplusg  16000  grpinvpropd  16091  grpsubpropd  16118  grpsubpropd2  16119  mulgpropd  16153  oppgmnd  16367  symgplusg  16392  sylow1lem2  16597  sylow3lem1  16625  prds1  17241  pwsmgp  17245  opprring  17258  rngidpropd  17322  dvdsrpropd  17323  unitpropd  17324  invrpropd  17325  rhm1  17357  lmhmpropd  17697  lidlrsppropd  17856  lpival  17871  rrgsuppOLD  17918  ressascl  17971  asclpropd  17973  aspval2  17974  psrbas  18008  psrbasOLD  18009  psrplusg  18012  psrmulr  18015  psrvscafval  18021  resspsrbas  18048  ressmplbas2  18095  opsrle  18118  opsrbaslem  18120  vr1val  18209  ressply1add  18249  ressply1mul  18250  ressply1vsca  18251  psrplusgpropd  18255  mplbaspropd  18256  psropprmul  18257  ply1baspropd  18262  ply1plusgpropd  18263  ply1sca2  18273  subrgvr1  18280  coe1mul2lem2  18287  ply1coe1eq  18318  zrhpropd  18529  znle  18550  frlmplusgval  18774  frlmvscafval  18776  mamudi  18882  mamudir  18883  matrcl  18891  oftpos  18931  mattpos1  18935  mdetfval  19065  mdetrlin  19081  mdetrsca  19082  mdetrsca2  19083  mdetrlin2  19086  mdetunilem5  19095  madufval  19116  madugsum  19122  idmatidpmat  19215  cpmidpmat  19351  cncmp  19869  2ndcsep  19937  llyeq  19948  nllyeq  19949  xkouni  20077  hmphindis  20275  xkocnv  20292  ptcmplem2  20530  snclseqg  20591  prdstmdd  20599  ustexsym  20695  ucnextcn  20784  metreslem  20842  comet  20993  nrmmetd  21072  nmpropd  21091  isngp3  21095  ngpds  21100  subgnm  21124  tngnm  21142  idnghm  21227  cnmetdval  21255  cnmpt2pc  21405  htpyco2  21456  phtpyco2  21467  clsocv  21667  rrxprds  21798  rrxnm  21800  ovolunlem1a  21884  voliunlem3  21939  ioombl1lem4  21948  uniioombllem4  21972  itg11  22075  itgeq1f  22155  itgeq2  22161  iblss2  22189  itgss  22195  itgeqa  22197  itgfsum  22210  itgsplit  22219  ditgeq1  22229  ditgeq2  22230  ditgeq3  22231  dvcmulf  22325  dvmptfsum  22353  dvcnvrelem2  22396  mdegfval  22437  mdegpropd  22461  deg1propd  22463  plyeq0  22585  coe11  22626  dgrlt  22639  dgradd2  22641  dgrmulc  22644  dvply1  22656  fta1lem  22679  pserulm  22793  rlimcnp2  23272  jensenlem1  23292  basellem5  23334  dchrbas  23486  dchrrcl  23491  dchrplusg  23498  dchrfi  23506  lgsdi  23583  lgseisenlem2  23601  lgsquadlem3  23607  dchrmusumlema  23654  rpvmasum2  23673  dchrisum0lema  23675  pntlemg  23759  colperpexlem2  24081  axlowdimlem13  24233  nbgraf1olem5  24421  nb3graprlem1  24427  constr2spthlem1  24572  constr3pthlem1  24631  constr3pthlem2  24632  avril1  25147  0vfval  25475  imsval  25567  imsdval  25568  bcseqi  26013  normpythi  26035  cm0  26503  fh1  26512  pjcji  26578  opsqrlem5  27039  pjsdi2i  27052  pjclem3  27092  pjci  27095  golem1  27166  iunrdx  27407  ofresid  27458  resmptf  27473  f1od2  27523  gsumvsca1  27750  gsumvsca2  27751  rhmopp  27786  resv1r  27804  crefeq  27825  xrge0mulc1cn  27900  qqhval2  27940  rrhre  27976  esumeq12dvaf  28021  esumeq2  28026  esumf1o  28038  esumfzf  28052  esumss  28055  esumpfinvalf  28059  ofceq  28073  itgeq12dv  28245  ccatmulgnn0dir  28473  cvmliftlem5  28711  cvmliftlem10  28716  cvmlift2lem9  28733  cvmliftphtlem  28739  mthmpps  28919  mpteq12d  29177  rdgprc  29202  dfrdg2  29203  predeq123  29220  trpredeq1  29278  trpredeq2  29279  trpredeq3  29280  wrecseq123  29312  wsuceq123  29345  wlimeq12  29350  symdifeq1  29445  symdifeq2  29446  altopthsn  29586  altxpeq1  29598  altxpeq2  29599  ee7.2aOLD  29901  finixpnum  30013  ptrest  30023  mbfposadd  30037  cnambfre  30038  iblabsnclem  30053  ftc1anclem1  30065  heiborlem4  30285  heiborlem6  30287  mpt2bi123f  30546  iineq12f  30548  mptbi12f  30550  imaiinfv  30600  mapfzcons1  30624  rexrabdioph  30702  dnnumch1  30965  dnwech  30969  aomclem6  30980  pwssplit4  31010  pwfi2f1o  31019  mendplusgfval  31110  mendvscafval  31115  dropab1  31310  dropab2  31311  itgsinexplem1  31642  wallispi2lem2  31743  fourierdlem36  31814  afveq12d  32056  aoveq123d  32101  aovfundmoveq  32104  aovnuoveq  32114  aovvoveq  32115  aovovn0oveq  32117  resisresindm  32143  fsumsplitsndif  32184  rngccofvalOLD  32535  ringccofvalOLD  32595  rhmsubclem2  32628  rhmsubcOLDlem2  32647  xpprsng  32654  csbfv12gALTOLD  33354  csbima12gALTOLD  33355  bnj956  33568  bnj1385  33624  bnj96  33656  bnj548  33688  bnj553  33689  bnj554  33690  bnj602  33706  bnj18eq1  33718  bnj1234  33802  bnj1296  33810  bnj1318  33814  bnj1442  33838  bnj1450  33839  bj-rabbida2  34233  bj-sngleq  34273  bj-tageq  34282  bj-projeq  34298  bj-projval  34302  bj-1upleq  34305  bj-pr1eq  34308  bj-pr2eq  34322  riotaclbgBAD  34425  toycom  34438  ldualvbase  34591  ldualfvadd  34593  ldualsca  34597  ldualsbase  34598  ldualsaddN  34599  ldualfvs  34601  ldual0  34612  ldual1  34613  ldualneg  34614  cdleme19f  35774  cdleme20m  35789  cdleme21k  35804  cdleme27b  35834  cdleme31so  35845  cdleme31sn  35846  cdleme31se  35848  cdleme31se2  35849  cdleme31sc  35850  cdleme31sde  35851  cdleme31fv  35856  cdleme40v  35935  cdleme43dN  35958  cdlemeg46ngfr  35984  ltrnco4  36205  tgrpbase  36212  tgrpopr  36213  erngbase  36267  erngfplus  36268  erngfmul  36271  erngbase-rN  36275  erngfplus-rN  36276  erngfmul-rN  36279  dvasca  36472  dvavbase  36479  dvafvadd  36480  dvafvsca  36482  tendocnv  36488  dvhsca  36549  dvhfplusr  36551  dvhvbase  36554  dvhfvadd  36558  dvhfvsca  36567  lcdvadd  37064  lcdsbase  37067  lcdsadd  37068  lcdvs  37070  lcd0  37075  lcd1  37076  lcdneg  37077  xpcogend  37466