Theorem 3eqtr4g 2797

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

Step	Hyp	Ref	Expression
1		3eqtr4g.2	. . 3 ⊢ 𝐶 = 𝐴
2		3eqtr4g.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	eqtrid 2784	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2790	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  rabbidva2  3402  rabbida4  3425  rabeqf  3434  csbeq1  3853  csbeq2  3855  csbeq2d  3856  csbeq2dv  3857  difeq1  4072  difeq2  4073  uneq2  4115  ineq1  4166  ineq2  4167  symdifeq1  4208  symdifeq2  4209  dfrab3ss  4276  csbprc  4362  csbnestgfw  4375  csbnestgf  4380  disjssun  4421  ifeq1  4484  ifeq2  4485  pweqALT  4570  sneq  4591  rabsneq  4600  csbsng  4666  csbprg  4667  preq1  4691  preq2  4692  tpeq1  4700  tpeq2  4701  tpeq3  4702  prprc1  4723  tpprceq3  4761  opeq1  4830  opeq2  4831  oteq1  4839  oteq2  4840  oteq3  4841  csbopg  4848  uniprg  4880  csbuni  4894  inteq  4906  iineq1  4965  iineq2  4968  iuneq12df  4974  iuneq12d  4977  dfiin2g  4987  iinrab  5025  iinin1  5035  iinxprg  5045  iununi  5055  opabbid  5164  opabbidv  5165  mpteq12da  5182  mpteq12f  5184  mpteq12dva  5185  csbmpt12  5506  xpeq1  5639  xpeq2  5646  rneq  5886  reseq1  5933  reseq2  5934  resima2  5976  resindm  5990  resmpt  5997  resmptf  5999  imaeq1  6015  imaeq2  6016  mptcnv  6097  xpdisj1  6120  xpdisj2  6121  resdisj  6128  dmpropg  6174  rnpropg  6181  cores  6208  cores2  6219  xpco  6248  predeq123  6261  csbpredg  6266  sspred  6269  predres  6298  suceqd  6385  sucprc  6396  iotaeq  6461  iotabi  6462  fntpg  6553  imain  6578  f1oprswap  6820  fveq1  6834  fveq2  6835  fvres  6854  csbfv12  6880  fnimapr  6918  fnimatpd  6919  fvco2  6932  xpprsng  7087  residpr  7090  fsnunfv  7135  fsnunres  7136  funiunfv  7196  f1ofvswap  7254  fliftf  7263  isoini2  7287  eqfunressuc  7309  riotaeqdv  7318  riotabidv  7319  riotauni  7323  riotabidva  7336  snriota  7350  oveq  7366  oveq1  7367  oveq2  7368  oprabbid  7425  oprabbidv  7426  mpoeq123  7432  mpoeq123dva  7434  mpoeq3dva  7437  resmpo  7480  ovres  7526  f1ocnvd  7611  ofeqd  7626  ofreq  7628  fpar  8060  frecseq123  8226  csbfrecsg  8228  wrecseq123  8257  csbwrecsg  8262  onovuni  8276  recseq  8307  tfr2a  8328  rdgeq1  8344  rdgeq2  8345  rdgsucmptf  8361  frsucmpt  8371  seqomeq12  8387  seqomsuc  8390  omopthi  8591  eceq1  8677  eceq2  8679  qseq1  8697  qseq2  8698  uniqs  8714  snecg  8718  ecinxp  8733  qsinxp  8734  erovlem  8754  ecopovtrn  8761  ixpeq1  8850  unfi  9099  supeq1  9352  supeq2  9355  supeq3  9356  supeq123d  9357  infeq1  9384  infeq2  9387  infeq3  9388  infeq123d  9389  infiso  9417  oieq1  9421  oieq2  9422  ordtypelem1  9427  inf3lemc  9539  wemapwe  9610  ttrcleq  9622  r1sucg  9685  r1limg  9687  rankprb  9767  karden  9811  djueq12  9820  cardiun  9898  acneq  9957  alephlim  9981  alephsuc  9982  alephfplem2  10019  infpssrlem2  10218  fin23lem34  10260  fin23lem35  10261  zorn2lem1  10410  zorn2lem7  10416  fpwwe2lem5  10550  fpwwe2lem12  10557  addpiord  10799  mulpiord  10800  addpqnq  10853  mulpqnq  10856  addassnq  10873  mulassnq  10874  distrnq  10876  lterpq  10885  ltexnq  10890  ltsrpr  10992  00sr  11014  recexsrlem  11018  mulgt0sr  11020  addcnsrec  11058  mulcnsrec  11059  negeq  11376  csbnegg  11381  negsubdi  11441  mulneg1  11577  negfi  12095  deceq1  12616  deceq2  12617  xnegeq  13126  fseq1p1m1  13518  om2uzrdg  13883  uzrdgsuci  13887  seqeq1  13931  seqeq2  13932  seqeq3  13933  seqfeq4  13978  seqof  13986  hashprg  14322  hashtpg  14412  csbwrdg  14471  s1eq  14528  cats1co  14783  s2eqd  14790  s3eqd  14791  s4eqd  14792  s5eqd  14793  s6eqd  14794  s7eqd  14795  s8eqd  14796  xpcogend  14901  shftval  15001  limsupgle  15404  lo1eq  15495  rlimeq  15496  sumeq1  15616  sumeq2w  15619  sumeq2ii  15620  sumeq2sdv  15630  zsum  15645  sumss2  15653  fsumsplitsnun  15682  isumclim3  15686  fsumcom2  15701  incexclem  15763  incexc2  15765  isumshft  15766  prodeq1f  15833  prodeq1  15834  prodeq2w  15837  prodeq2ii  15838  prodeq2sdv  15850  zprod  15864  fprodm1s  15897  fprodp1s  15898  fprodcom2  15911  fprodsplitf  15915  iprodclim3  15927  ef0lem  16005  ruclem7  16165  sadcp1  16386  smupp1  16411  smueqlem  16421  algrp1  16505  dfphi2  16705  prmdiveq  16717  pceulem  16777  vdwlem6  16918  cshwsiun  17031  sloteq  17114  setsid  17138  elbasfv  17146  elbasov  17147  imastset  17447  imasvscaval  17463  isoval  17693  funcoppc  17803  fulloppc  17852  fuccofval  17890  natpropd  17907  catccofval  18032  xpchomfval  18106  xpccofval  18109  lubfval  18275  glbfval  18288  chneq1  18539  chneq2  18540  grpidpropd  18591  gsumpropd2lem  18608  frmdplusg  18783  efmndplusg  18809  grpinvpropd  18949  grpsubpropd  18979  grpsubpropd2  18980  mulgpropd  19050  ecqusaddd  19125  oppgmnd  19287  sylow1lem2  19532  sylow3lem1  19560  prds1  20262  pwsmgp  20266  opprrng  20285  rngidpropd  20355  dvdsrpropd  20356  unitpropd  20357  invrpropd  20358  rhm1  20428  rhmopp  20446  rhmsubclem2  20623  lmhmpropd  21029  lidlrsppropd  21203  rngqiprnglinlem2  21251  lpival  21283  pzriprnglem11  21450  zrhpropd  21473  znle  21495  frlmplusgval  21723  frlmvscafval  21725  ressascl  21856  asclpropd  21857  aspval2  21858  psrbas  21893  psrplusg  21896  psrmulr  21902  psrvscafval  21908  resspsrbas  21933  ressmplbas2  21986  opsrle  22006  opsrbaslem  22008  vr1val  22136  ressply1add  22174  ressply1mul  22175  ressply1vsca  22176  psrplusgpropd  22180  mplbaspropd  22181  psropprmul  22182  ply1baspropd  22187  ply1plusgpropd  22188  ply1sca2  22198  ply1ascl0  22199  ply1ascl1  22200  subrgvr1  22207  coe1mul2lem2  22214  ply1coe1eq  22248  evls1addd  22319  evls1muld  22320  evls1vsca  22321  rhmply1vr1  22335  rhmply1vsca  22336  mamudi  22351  mamudir  22352  matrcl  22360  oftpos  22400  mattpos1  22404  mdetfval  22534  mdetrlin  22550  mdetrsca  22551  mdetrsca2  22552  mdetrlin2  22555  mdetunilem5  22564  madufval  22585  madugsum  22591  idmatidpmat  22685  cpmidpmat  22821  cncmp  23340  2ndcsep  23407  llyeq  23418  nllyeq  23419  xkouni  23547  hmphindis  23745  xkocnv  23762  ptcmplem2  24001  snclseqg  24064  prdstmdd  24072  ustexsym  24164  ucnextcn  24251  metreslem  24310  comet  24461  nrmmetd  24522  nmpropd  24542  isngp3  24546  ngpds  24552  subgnm  24581  tngnm  24599  idnghm  24691  cnmetdval  24718  cnmpopc  24882  htpyco2  24938  phtpyco2  24949  clsocv  25210  rrxprds  25349  rrxnm  25351  rrxplusgvscavalb  25355  ovolunlem1a  25457  voliunlem3  25513  ioombl1lem4  25522  uniioombllem4  25547  itg11  25652  itgeq1f  25732  itgeq1fOLD  25733  itgeq1  25734  itgeq2  25739  iblss2  25767  itgss  25773  itgeqa  25775  itgfsum  25788  itgsplit  25797  ditgeq1  25809  ditgeq2  25810  ditgeq3  25811  dvcmulf  25908  dvmptfsum  25939  dvcnvrelem2  25983  mdegfval  26027  mdegpropd  26049  deg1propd  26051  plyeq0  26176  coe11  26218  dgrlt  26232  dgradd2  26234  dgrmulc  26237  dvply1  26251  fta1lem  26275  pserulm  26391  rlimcnp2  26936  jensenlem1  26957  basellem5  27055  dchrbas  27206  dchrrcl  27211  dchrplusg  27218  dchrfi  27226  lgsdi  27305  lgseisenlem2  27347  lgsquadlem3  27353  dchrmusumlema  27464  rpvmasum2  27483  dchrisum0lema  27485  pntlemg  27569  nosupbnd2lem1  27687  lruneq  27907  addsval  27962  mulsval  28109  seqseq123d  28286  colperpexlem2  28807  axlowdimlem13  29031  uhgrvtxedgiedgb  29213  nb3grprlem1  29457  crctcshlem2  29895  wpthswwlks2on  30041  clwlknf1oclwwlkn  30163  frgrncvvdeq  30388  avril1  30542  0vfval  30685  imsval  30764  imsdval  30765  bcseqi  31199  normpythi  31221  cm0  31688  fh1  31697  pjcji  31763  opsqrlem5  32223  pjsdi2i  32236  pjclem3  32276  pjci  32279  golem1  32350  iuneq12daf  32634  iunrdx  32641  ofresid  32723  cnvprop  32777  coprprop  32780  f1od2  32800  dp2eq1  32956  dp2eq2  32957  fzto1st1  33186  gsumvsca1  33310  gsumvsca2  33311  urpropd  33315  resv1r  33422  nsgqusf1olem2  33497  oppr2idl  33569  opprqus0g  33573  ressply1evls1  33648  esplyfvn  33735  vietalem  33737  lindsunlem  33783  fedgmullem1  33788  fedgmullem2  33789  fedgmul  33790  fldsdrgfldext2  33821  fldextrspunlem1  33834  fldextrspunfld  33835  algextdeglem4  33879  crefeq  34004  rspectopn  34026  xrge0mulc1cn  34100  qqhval2  34141  esumeq12dvaf  34190  esumeq2  34195  esumf1o  34209  esumfzf  34228  esumss  34231  esumpfinvalf  34235  ofceq  34256  carsgclctunlem1  34476  itgeq12dv  34485  ccatmulgnn0dir  34701  breprexpnat  34793  bnj956  34934  bnj1385  34990  bnj96  35023  bnj548  35055  bnj553  35056  bnj554  35057  bnj602  35073  bnj18eq1  35085  bnj1234  35171  bnj1296  35179  bnj1318  35183  bnj1442  35207  bnj1450  35208  cvmliftlem5  35485  cvmliftlem10  35490  cvmlift2lem9  35507  cvmliftphtlem  35513  satfdm  35565  mthmpps  35778  rdgprc  35988  dfrdg2  35989  wsuceq123  36008  wlimeq12  36013  altopthsn  36157  altxpeq1  36169  altxpeq2  36170  ixpeq12dv  36412  prodeq12sdv  36414  itgeq12sdv  36415  ditgeq123dv  36417  cbvcsbdavw  36455  cbvcsbdavw2  36456  cbvrabdavw  36457  cbviundavw  36458  cbviindavw  36459  cbvopab1davw  36460  cbvopab2davw  36461  cbvopabdavw  36462  cbvmptdavw  36463  cbviotadavw  36465  cbvriotadavw  36466  cbvoprab1davw  36467  cbvoprab2davw  36468  cbvoprab3davw  36469  cbvoprab123davw  36470  cbvoprab12davw  36471  cbvoprab23davw  36472  cbvoprab13davw  36473  cbvixpdavw  36474  cbvsumdavw  36475  cbvproddavw  36476  cbvitgdavw  36477  cbvditgdavw  36478  cbvrabdavw2  36481  cbviundavw2  36482  cbviindavw2  36483  cbvmptdavw2  36484  cbvriotadavw2  36486  cbvmpodavw2  36487  cbvmpo1davw2  36488  cbvmpo2davw2  36489  cbvixpdavw2  36490  cbvsumdavw2  36491  cbvproddavw2  36492  cbvitgdavw2  36493  cbvditgdavw2  36494  ee7.2aOLD  36657  bj-sngleq  37170  bj-tageq  37179  bj-projeq  37195  bj-projval  37199  bj-1upleq  37202  bj-pr1eq  37205  bj-pr2eq  37219  bj-evaleq  37279  bj-imafv  37458  csbrecsg  37535  csbrdgg  37536  csboprabg  37537  csbmpo123  37538  finxpeq1  37593  finxpeq2  37594  csbfinxpg  37595  finxpreclem4  37601  cureq  37799  unceq  37800  uncov  37804  unccur  37806  finixpnum  37808  ptrest  37822  poimirlem3  37826  poimirlem9  37832  poimirlem15  37838  poimirlem16  37839  poimirlem26  37849  poimirlem27  37850  mbfposadd  37870  cnambfre  37871  iblabsnclem  37886  ftc1anclem1  37896  heiborlem4  38017  heiborlem6  38019  mpobi123f  38365  iineq12f  38367  mptbi12f  38369  eccnvepres  38489  xrneq1  38599  xrneq2  38602  shiftstableeq2  38686  cosseq  38719  redundss3  38915  riotaclbgBAD  39282  toycom  39301  ldualvbase  39454  ldualfvadd  39456  ldualsca  39460  ldualsbase  39461  ldualsaddN  39462  ldualfvs  39464  ldual0  39475  ldual1  39476  ldualneg  39477  cdleme19f  40636  cdleme20m  40651  cdleme21k  40666  cdleme27b  40696  cdleme31so  40707  cdleme31sn  40708  cdleme31se  40710  cdleme31se2  40711  cdleme31sc  40712  cdleme31sde  40713  cdleme31fv  40718  cdleme40v  40797  cdleme43dN  40820  cdlemeg46ngfr  40846  ltrnco4  41067  tgrpbase  41074  tgrpopr  41075  erngbase  41129  erngfplus  41130  erngfmul  41133  erngbase-rN  41137  erngfplus-rN  41138  erngfmul-rN  41141  dvasca  41334  dvavbase  41341  dvafvadd  41342  dvafvsca  41344  tendocnv  41349  dvhsca  41410  dvhfplusr  41412  dvhvbase  41415  dvhfvadd  41419  dvhfvsca  41428  lcdvadd  41925  lcdsbase  41928  lcdsadd  41929  lcdvs  41931  lcd0  41936  lcd1  41937  lcdneg  41938  fsuppind  42900  imaiinfv  43002  mapfzcons1  43026  rexrabdioph  43103  dnnumch1  43353  dnwech  43357  aomclem6  43368  pwssplit4  43398  pwfi2f1o  43405  mendplusgfval  43490  mendvscafval  43495  harval3  43846  dssmapntrcls  44436  scotteqd  44545  colleq12d  44561  uzmptshftfval  44654  dropab1  44754  dropab2  44755  iineq12dv  45417  rabbida2  45443  rabbida3  45446  itgsinexplem1  46265  wallispi2lem2  46383  fourierdlem36  46454  etransclem4  46549  fcoreslem1  47376  afveq12d  47446  aoveq123d  47491  aovfundmoveq  47494  aovnuoveq  47504  aovvoveq  47505  aovovn0oveq  47507  afv2eq12d  47528  fsumsplitsndif  47686  rngccofvalALTV  48583  rhmsubcALTVlem2  48595  ringccofvalALTV  48617  itscnhlinecirc02plem2  49096  oppfrcl3  49442  oppf1st2nd  49443  uppropd  49493  natoppf  49541  catcrcl  49707  lmdpropd  49969  cmdpropd  49970  lmddu  49979  cmddu  49980  setrecseq  49997  aacllem  50113