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 1541

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  rabbidva2  3434  rabbida4  3457  rabeqf  3466  rabeqiOLD  3471  csbeq1  3895  csbeq2  3897  csbeq2d  3898  difeq1  4114  difeq2  4115  uneq2  4156  ineq1  4204  ineq2  4205  symdifeq1  4243  symdifeq2  4244  dfrab3ss  4311  csbprc  4405  csbnestgfw  4418  csbnestgf  4423  disjssun  4466  ifeq1  4531  ifeq2  4532  pweqALT  4616  sneq  4637  csbsng  4711  csbprg  4712  preq1  4736  preq2  4737  tpeq1  4745  tpeq2  4746  tpeq3  4747  prprc1  4768  tpprceq3  4806  opeq1  4872  opeq2  4873  oteq1  4881  oteq2  4882  oteq3  4883  csbopg  4890  unieqOLD  4919  uniprg  4924  csbuni  4939  inteq  4952  iineq1  5013  iineq2  5016  iuneq12df  5022  dfiin2g  5034  iinrab  5071  iinin1  5081  iinxprg  5091  iununi  5101  opabbid  5212  opabbidv  5213  mpteq12da  5232  mpteq12dfOLD  5234  mpteq12f  5235  mpteq12dva  5236  csbmpt12  5556  xpeq1  5689  xpeq2  5696  rneq  5933  reseq1  5973  reseq2  5974  resima2  6014  resindm  6028  resmpt  6035  resmptf  6037  imaeq1  6052  imaeq2  6053  mptcnv  6136  xpdisj1  6157  xpdisj2  6158  resdisj  6165  dmpropg  6211  rnpropg  6218  cores  6245  cores2  6255  xpco  6285  predeq123  6298  csbpredg  6303  sspred  6306  predres  6337  suceq  6427  sucprc  6437  iotaeq  6505  iotabi  6506  fntpg  6605  imain  6630  f1oprswap  6874  fveq1  6887  fveq2  6888  fvres  6907  csbfv12  6936  fnimapr  6972  fvco2  6985  xpprsng  7134  residpr  7137  fsnunfv  7181  fsnunres  7182  funiunfv  7243  f1ofvswap  7300  fliftf  7308  isoini2  7332  eqfunressuc  7354  riotaeqdv  7362  riotabidv  7363  riotauni  7367  riotabidva  7381  snriota  7395  oveq  7411  oveq1  7412  oveq2  7413  oprabbid  7470  oprabbidv  7471  mpoeq123  7477  mpoeq123dva  7479  mpoeq3dva  7482  resmpo  7524  ovres  7569  f1ocnvd  7653  ofeqd  7668  ofreq  7670  fpar  8098  frecseq123  8263  csbfrecsg  8265  wrecseq123  8295  wrecseq123OLD  8296  csbwrecsg  8302  onovuni  8338  recseq  8370  tfr2a  8391  rdgeq1  8407  rdgeq2  8408  rdgsucmptf  8424  frsucmpt  8434  seqomeq12  8450  seqomsuc  8453  omopthi  8656  eceq1  8737  eceq2  8739  qseq1  8753  qseq2  8754  uniqs  8767  ecinxp  8782  qsinxp  8783  erovlem  8803  ecopovtrn  8810  ixpeq1  8898  unfi  9168  supeq1  9436  supeq2  9439  supeq3  9440  supeq123d  9441  infeq1  9467  infeq2  9470  infeq3  9471  infeq123d  9472  infiso  9499  oieq1  9503  oieq2  9504  ordtypelem1  9509  inf3lemc  9617  wemapwe  9688  ttrcleq  9700  r1sucg  9760  r1limg  9762  rankprb  9842  karden  9886  djueq12  9895  cardiun  9973  acneq  10034  alephlim  10058  alephsuc  10059  alephfplem2  10096  infpssrlem2  10295  fin23lem34  10337  fin23lem35  10338  zorn2lem1  10487  zorn2lem7  10493  fpwwe2lem5  10626  fpwwe2lem12  10633  addpiord  10875  mulpiord  10876  addpqnq  10929  mulpqnq  10932  addassnq  10949  mulassnq  10950  distrnq  10952  lterpq  10961  ltexnq  10966  ltsrpr  11068  00sr  11090  recexsrlem  11094  mulgt0sr  11096  addcnsrec  11134  mulcnsrec  11135  negeq  11448  csbnegg  11453  negsubdi  11512  mulneg1  11646  negfi  12159  deceq1  12678  deceq2  12679  xnegeq  13182  fseq1p1m1  13571  om2uzrdg  13917  uzrdgsuci  13921  seqeq1  13965  seqeq2  13966  seqeq3  13967  seqfeq4  14013  seqof  14021  hashprg  14351  hashtpg  14442  csbwrdg  14490  s1eq  14546  cats1co  14803  s2eqd  14810  s3eqd  14811  s4eqd  14812  s5eqd  14813  s6eqd  14814  s7eqd  14815  s8eqd  14816  xpcogend  14917  shftval  15017  limsupgle  15417  lo1eq  15508  rlimeq  15509  sumeq1  15631  sumeq2w  15634  sumeq2ii  15635  zsum  15660  sumss2  15668  fsumsplitsnun  15697  isumclim3  15701  fsumcom2  15716  incexclem  15778  incexc2  15780  isumshft  15781  prodeq1f  15848  prodeq2w  15852  prodeq2ii  15853  zprod  15877  fprodm1s  15910  fprodp1s  15911  fprodcom2  15924  fprodsplitf  15928  iprodclim3  15940  ef0lem  16018  ruclem7  16175  sadcp1  16392  smupp1  16417  smueqlem  16427  algrp1  16507  dfphi2  16703  prmdiveq  16715  pceulem  16774  vdwlem6  16915  cshwsiun  17029  sloteq  17112  setsid  17137  elbasfv  17146  elbasov  17147  imastset  17464  imasvscaval  17480  isoval  17708  funcoppc  17821  fulloppc  17869  fuccofval  17907  natpropd  17925  catccofval  18050  xpchomfval  18127  xpccofval  18130  lubfval  18299  glbfval  18312  grpidpropd  18577  gsumpropd2lem  18594  frmdplusg  18731  efmndplusg  18757  grpinvpropd  18894  grpsubpropd  18924  grpsubpropd2  18925  mulgpropd  18990  oppgmnd  19215  sylow1lem2  19461  sylow3lem1  19489  prds1  20129  pwsmgp  20133  opprring  20153  rngidpropd  20221  dvdsrpropd  20222  unitpropd  20223  invrpropd  20224  rhm1  20259  rhmopp  20280  lmhmpropd  20676  lidlrsppropd  20847  lpival  20875  zrhpropd  21055  znle  21079  frlmplusgval  21310  frlmvscafval  21312  ressascl  21441  asclpropd  21442  aspval2  21443  psrbas  21488  psrplusg  21491  psrmulr  21494  psrvscafval  21500  resspsrbas  21526  ressmplbas2  21573  opsrle  21593  opsrbaslem  21595  opsrbaslemOLD  21596  vr1val  21707  ressply1add  21743  ressply1mul  21744  ressply1vsca  21745  psrplusgpropd  21749  mplbaspropd  21750  psropprmul  21751  ply1baspropd  21756  ply1plusgpropd  21757  ply1sca2  21767  subrgvr1  21774  coe1mul2lem2  21781  ply1coe1eq  21813  mamudi  21894  mamudir  21895  matrcl  21903  oftpos  21945  mattpos1  21949  mdetfval  22079  mdetrlin  22095  mdetrsca  22096  mdetrsca2  22097  mdetrlin2  22100  mdetunilem5  22109  madufval  22130  madugsum  22136  idmatidpmat  22230  cpmidpmat  22366  cncmp  22887  2ndcsep  22954  llyeq  22965  nllyeq  22966  xkouni  23094  hmphindis  23292  xkocnv  23309  ptcmplem2  23548  snclseqg  23611  prdstmdd  23619  ustexsym  23711  ucnextcn  23800  metreslem  23859  comet  24013  nrmmetd  24074  nmpropd  24094  isngp3  24098  ngpds  24104  subgnm  24133  tngnm  24159  idnghm  24251  cnmetdval  24278  cnmpopc  24435  htpyco2  24486  phtpyco2  24497  clsocv  24758  rrxprds  24897  rrxnm  24899  rrxplusgvscavalb  24903  ovolunlem1a  25004  voliunlem3  25060  ioombl1lem4  25069  uniioombllem4  25094  itg11  25199  itgeq1f  25280  itgeq2  25286  iblss2  25314  itgss  25320  itgeqa  25322  itgfsum  25335  itgsplit  25344  ditgeq1  25356  ditgeq2  25357  ditgeq3  25358  dvcmulf  25453  dvmptfsum  25483  dvcnvrelem2  25526  mdegfval  25571  mdegpropd  25593  deg1propd  25595  plyeq0  25716  coe11  25758  dgrlt  25771  dgradd2  25773  dgrmulc  25776  dvply1  25788  fta1lem  25811  pserulm  25925  rlimcnp2  26460  jensenlem1  26480  basellem5  26578  dchrbas  26727  dchrrcl  26732  dchrplusg  26739  dchrfi  26747  lgsdi  26826  lgseisenlem2  26868  lgsquadlem3  26874  dchrmusumlema  26985  rpvmasum2  27004  dchrisum0lema  27006  pntlemg  27090  nosupbnd2lem1  27207  lruneq  27389  addsval  27435  mulsval  27554  colperpexlem2  27971  axlowdimlem13  28201  uhgrvtxedgiedgb  28385  nb3grprlem1  28626  crctcshlem2  29061  wpthswwlks2on  29204  clwlknf1oclwwlkn  29326  frgrncvvdeq  29551  avril1  29705  0vfval  29846  imsval  29925  imsdval  29926  bcseqi  30360  normpythi  30382  cm0  30849  fh1  30858  pjcji  30924  opsqrlem5  31384  pjsdi2i  31397  pjclem3  31437  pjci  31440  golem1  31511  iuneq12daf  31775  iunrdx  31782  ofresid  31854  fnimatp  31889  cnvprop  31905  coprprop  31908  f1od2  31933  dp2eq1  32026  dp2eq2  32027  fzto1st1  32248  gsumvsca1  32358  gsumvsca2  32359  urpropd  32365  resv1r  32444  nsgqusf1olem2  32513  oppr2idl  32588  opprqus0g  32592  evls1addd  32636  evls1muld  32637  evls1vsca  32638  ply1ascl0  32640  ply1ascl1  32641  lindsunlem  32697  fedgmullem1  32702  fedgmullem2  32703  fedgmul  32704  algextdeglem1  32760  crefeq  32813  rspectopn  32835  xrge0mulc1cn  32909  qqhval2  32950  esumeq12dvaf  33017  esumeq2  33022  esumf1o  33036  esumfzf  33055  esumss  33058  esumpfinvalf  33062  ofceq  33083  carsgclctunlem1  33304  itgeq12dv  33313  ccatmulgnn0dir  33541  breprexpnat  33634  bnj956  33775  bnj1385  33831  bnj96  33864  bnj548  33896  bnj553  33897  bnj554  33898  bnj602  33914  bnj18eq1  33926  bnj1234  34012  bnj1296  34020  bnj1318  34024  bnj1442  34048  bnj1450  34049  cvmliftlem5  34268  cvmliftlem10  34273  cvmlift2lem9  34290  cvmliftphtlem  34296  satfdm  34348  mthmpps  34561  rdgprc  34754  dfrdg2  34755  wsuceq123  34774  wlimeq12  34779  altopthsn  34921  altxpeq1  34933  altxpeq2  34934  ee7.2aOLD  35334  bj-sngleq  35836  bj-tageq  35845  bj-projeq  35861  bj-projval  35865  bj-1upleq  35868  bj-pr1eq  35871  bj-pr2eq  35885  bj-evaleq  35941  bj-imafv  36120  csbrecsg  36197  csbrdgg  36198  csboprabg  36199  csbmpo123  36200  finxpeq1  36255  finxpeq2  36256  csbfinxpg  36257  finxpreclem4  36263  cureq  36452  unceq  36453  uncov  36457  unccur  36459  finixpnum  36461  ptrest  36475  poimirlem3  36479  poimirlem9  36485  poimirlem15  36491  poimirlem16  36492  poimirlem26  36502  poimirlem27  36503  mbfposadd  36523  cnambfre  36524  iblabsnclem  36539  ftc1anclem1  36549  heiborlem4  36670  heiborlem6  36672  mpobi123f  37018  iineq12f  37020  mptbi12f  37022  eccnvepres  37136  uniqsALTV  37186  xrneq1  37235  xrneq2  37238  cosseq  37284  redundss3  37486  riotaclbgBAD  37812  toycom  37831  ldualvbase  37984  ldualfvadd  37986  ldualsca  37990  ldualsbase  37991  ldualsaddN  37992  ldualfvs  37994  ldual0  38005  ldual1  38006  ldualneg  38007  cdleme19f  39167  cdleme20m  39182  cdleme21k  39197  cdleme27b  39227  cdleme31so  39238  cdleme31sn  39239  cdleme31se  39241  cdleme31se2  39242  cdleme31sc  39243  cdleme31sde  39244  cdleme31fv  39249  cdleme40v  39328  cdleme43dN  39351  cdlemeg46ngfr  39377  ltrnco4  39598  tgrpbase  39605  tgrpopr  39606  erngbase  39660  erngfplus  39661  erngfmul  39664  erngbase-rN  39668  erngfplus-rN  39669  erngfmul-rN  39672  dvasca  39865  dvavbase  39872  dvafvadd  39873  dvafvsca  39875  tendocnv  39880  dvhsca  39941  dvhfplusr  39943  dvhvbase  39946  dvhfvadd  39950  dvhfvsca  39959  lcdvadd  40456  lcdsbase  40459  lcdsadd  40460  lcdvs  40462  lcd0  40467  lcd1  40468  lcdneg  40469  fsuppind  41159  imaiinfv  41416  mapfzcons1  41440  rexrabdioph  41517  dnnumch1  41771  dnwech  41775  aomclem6  41786  pwssplit4  41816  pwfi2f1o  41823  mendplusgfval  41912  mendvscafval  41917  harval3  42274  dssmapntrcls  42864  scotteqd  42981  colleq12d  42997  uzmptshftfval  43090  dropab1  43191  dropab2  43192  rabbida2  43806  rabbida3  43809  itgsinexplem1  44656  wallispi2lem2  44774  fourierdlem36  44845  etransclem4  44940  fcoreslem1  45759  afveq12d  45827  aoveq123d  45872  aovfundmoveq  45875  aovnuoveq  45885  aovvoveq  45886  aovovn0oveq  45888  afv2eq12d  45909  fsumsplitsndif  46027  opprrng  46660  ecqusadd  46749  rngqiprnglinlem2  46757  rngccofvalALTV  46838  ringccofvalALTV  46901  rhmsubclem2  46938  rhmsubcALTVlem2  46956  itscnhlinecirc02plem2  47422  setrecseq  47683  aacllem  47801