Theorem 3eqtr4g 2823

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 2810	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2816	1 ⊢ (𝜑 → 𝐶 = 𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  rabbidva2  3418  rabbida4  3440  csbeq1  3854  csbeq2  3856  csbeq2d  3857  csbeq2dv  3858  difeq1  4059  difeq2  4060  ineq1  4113  ineq2  4114  uneq2  4164  symdifeq1  4203  symdifeq2  4204  dfrab3ss  4271  csbprc  4370  csbnestgfw  4383  csbnestgf  4388  disjssun  4424  ifeq1  4489  ifeq2  4490  pweqALT  4575  sneq  4594  csbsng  4669  csbprg  4670  preq1  4694  preq2  4695  tpeq1  4703  tpeq2  4704  tpeq3  4705  prprc1  4726  tpprceq3  4767  opeq1  4843  opeq2  4844  csbopg  4854  oteq1  4863  oteq2  4864  oteq3  4865  uniprg  4886  csbuni  4901  inteq  4913  iineq1  4972  iineq2  4975  iuneq12df  4981  iuneq12d  4983  dfiin2g  4992  iinrab  5030  iinin1  5042  iinxprg  5052  iununi  5062  opabbid  5173  opabbidv  5174  mpteq12da  5191  mpteq12f  5193  mpteq12dva  5194  csbmpt12  5536  xpeq1  5669  xpeq2  5676  rneq  5924  reseq1  5974  reseq2  5975  resindmOLD  6031  resmpt  6040  resmptf  6042  imaeq1  6058  imaeq2  6059  resima2  6068  dfrn7  6077  mptcnv  6143  xpdisj1  6163  xpdisj2  6164  resdisj  6172  dmpropg  6228  rnpropg  6235  cores  6262  cores2  6273  xpco  6307  predeq123  6320  csbpredg  6325  sspred  6328  predres  6357  suceqd  6445  sucprc  6456  iotaeq  6521  iotabi  6522  fntpg  6619  imain  6644  f1oprswap  6890  fveq1  6904  fveq2  6905  fvres  6924  csbfv12  6950  fnimapr  6988  fnimatpd  6989  fvco2  7002  xpprsng  7163  xpsnprg  7164  xpsntpg  7165  residpr  7167  fsnunfv  7212  fsnunres  7213  funiunfv  7272  f1ofvswap  7334  fliftf  7343  isoini2  7367  eqfunressuc  7391  riotaeqdv  7398  riotabidv  7399  riotauni  7403  riotabidva  7416  snriota  7430  oveq  7446  oveq1  7447  oveq2  7448  oprabbid  7505  oprabbidv  7506  mpoeq123  7512  mpoeq123dva  7514  mpoeq3dva  7517  resmpo  7560  ovres  7607  f1ocnvd  7693  mpt3eqdv  7707  ofeqd  7716  ofreq  7718  f1od2  8132  fpar  8151  frecseq123  8325  csbfrecsg  8327  wrecseq123  8356  csbwrecsg  8361  onovuni  8375  recseq  8406  tfr2a  8428  rdgeq1  8444  rdgeq2  8445  rdgsucmptf  8461  frsucmpt  8471  seqomeq12  8489  seqomsuc  8492  omopthi  8695  eceq1  8782  eceq2  8784  qseq1  8802  qseq2  8803  uniqs  8819  snecg  8823  ecinxp  8838  qsinxp  8839  erovlem  8859  ecopovtrn  8866  cureq  8914  uncov  8918  ixpeq1  8961  unfi  9211  supeq1  9461  supeq2  9464  supeq3  9465  supeq123d  9466  infeq1  9493  infeq2  9496  infeq3  9497  infeq123d  9498  infiso  9526  oieq1  9530  oieq2  9531  ordtypelem1  9536  inf3lemc  9651  wemapwe  9722  ttrcleq  9734  r1sucg  9800  r1limg  9802  rankprb  9889  scotteqd  9954  karden  9983  kardenOLD  9984  djueq12  10009  cardiun  10087  acneq  10146  alephlim  10170  alephsuc  10171  alephfplem2  10208  infpssrlem2  10406  fin23lem34  10448  fin23lem35  10449  zorn2lem1  10598  zorn2lem7  10604  fpwwe2lem5  10744  fpwwe2lem12  10751  addpiord  10993  mulpiord  10994  addpqnq  11047  mulpqnq  11050  addassnq  11067  mulassnq  11068  distrnq  11070  lterpq  11079  ltexnq  11084  ltsrpr  11186  00sr  11208  recexsrlem  11212  mulgt0sr  11214  addcnsrec  11252  mulcnsrec  11253  negeq  11573  csbnegg  11578  negsubdi  11638  mulneg1  11776  negfi  12290  deceq1  12843  deceq2  12844  xnegeq  13361  fseq1p1m1  13756  om2uzrdg  14123  uzrdgsuci  14127  seqeq1  14171  seqeq2  14172  seqeq3  14173  seqfeq4  14218  seqof  14226  hashprg  14563  hashtpg  14654  csbwrdg  14713  s1eq  14771  cats1co  15032  s2eqd  15039  s3eqd  15040  s4eqd  15041  s5eqd  15042  s6eqd  15043  s7eqd  15044  s8eqd  15045  xpcogend  15153  shftval  15253  limsupgle  15670  lo1eq  15761  rlimeq  15762  sumeq1  15882  sumeq2w  15885  sumeq2ii  15886  sumeq2sdv  15896  zsum  15910  sumss2  15918  fsumsplitsnun  15947  isumclim3  15951  fsumcom2  15966  incexclem  16031  incexc2  16033  isumshft  16034  prodeq1f  16101  prodeq1  16102  prodeq2w  16105  prodeq2ii  16106  prodeq2sdv  16117  zprod  16130  fprodm1s  16163  fprodp1s  16164  fprodcom2  16177  fprodsplitf  16181  iprodclim3  16193  ef0lem  16270  ruclem7  16430  sadcp1  16651  smupp1  16676  smueqlem  16686  algrp1  16775  dfphi2  16977  prmdiveq  16989  pceulem  17049  vdwlem6  17190  cshwsiun  17303  sloteq  17387  setsid  17411  elbasfv  17419  elbasov  17420  imastset  17720  imasvscaval  17736  isoval  17966  funcoppc  18076  fulloppc  18125  fuccofval  18163  natpropd  18180  catccofval  18305  xpchomfval  18379  xpccofval  18382  lubfval  18548  glbfval  18561  chneq1  18812  chneq2  18813  grpidpropd  18868  gsumpropd2lem  18894  frmdplusg  19076  efmndplusg  19102  grpinvpropd  19251  grpsubpropd  19281  grpsubpropd2  19282  mulgpropd  19352  ecqusaddd  19433  oppgmnd  19595  sylow1lem2  19840  sylow3lem1  19868  prds1  20579  pwsmgp  20583  opprrng  20602  rngidpropd  20672  dvdsrpropd  20673  unitpropd  20674  invrpropd  20675  rhm1  20751  rhmopp  20786  rhmsubclem2  20965  lmhmpropd  21375  lidlrsppropd  21559  rngqiprnglinlem2  21615  lpival  21675  pzriprnglem11  21824  zrhpropd  21847  znle  21869  frlmplusgval  22097  frlmvscafval  22099  ressascl  22231  asclpropd  22232  aspval2  22233  psrbas  22269  psrplusg  22272  psrmulr  22277  psrvscafval  22283  resspsrbas  22308  ressmplbas2  22362  opsrle  22383  opsrbaslem  22385  vr1val  22537  ressply1add  22574  ressply1mul  22575  ressply1vsca  22576  psrplusgpropd  22580  mplbaspropd  22581  psropprmul  22582  ply1baspropd  22587  ply1plusgpropd  22588  ply1sca2  22598  ply1ascl0  22599  ply1ascl1  22600  subrgvr1  22607  coe1mul2lem2  22614  ply1coe1eq  22645  evls1addd  22716  evls1muld  22717  evls1vsca  22718  rhmply1vr1  22729  rhmply1vsca  22730  mamudi  22745  mamudir  22746  matrcl  22754  oftpos  22794  mattpos1  22798  mdetfval  22928  mdetrlin  22944  mdetrsca  22945  mdetrsca2  22946  mdetrlin2  22949  mdetunilem5  22958  madufval  22979  madugsum  22985  idmatidpmat  23082  cpmidpmat  23218  cncmp  23737  2ndcsep  23805  llyeq  23816  nllyeq  23817  xkouni  23945  hmphindis  24143  xkocnv  24160  ptcmplem2  24399  snclseqg  24462  prdstmdd  24470  ustexsym  24562  ucnextcn  24649  metreslem  24708  comet  24859  nrmmetd  24920  nmpropd  24940  isngp3  24944  ngpds  24950  subgnm  24979  tngnm  24997  idnghm  25089  cnmetdval  25116  cnmpopc  25276  htpyco2  25327  phtpyco2  25338  clsocv  25598  rrxprds  25737  rrxnm  25739  rrxplusgvscavalb  25743  ovolunlem1a  25844  voliunlem3  25900  ioombl1lem4  25909  uniioombllem4  25934  itg11  26039  itgeq1f  26119  itgeq1  26120  itgeq2  26125  iblss2  26153  itgss  26159  itgeqa  26161  itgfsum  26174  itgsplit  26183  ditgeq1  26195  ditgeq2  26196  ditgeq3  26197  dvcmulf  26292  dvmptfsum  26322  dvcnvrelem2  26365  mdegfval  26407  mdegpropd  26429  deg1propd  26431  plyeq0  26557  coe11  26599  dgrlt  26612  dgradd2  26614  dgrmulc  26617  dvply1  26632  fta1lem  26655  pserulm  26776  rlimcnp2  27321  jensenlem1  27341  basellem5  27439  dchrbas  27589  dchrrcl  27594  dchrplusg  27601  dchrfi  27609  lgsdi  27688  lgseisenlem2  27730  lgsquadlem3  27736  dchrmusumlema  27847  rpvmasum2  27866  dchrisum0lema  27868  pntlemg  27952  nosupbnd2lem1  28099  lruneq  28320  addsval  28375  mulsval  28522  seqseq123d  28699  colperpexlem2  29234  symquadmid  29331  tgaaddcpbllem2  29377  axlowdimlem13  29559  uhgrvtxedgiedgb  29741  nb3grprlem1  29988  crctcshlem2  30434  wpthswwlks2on  30580  clwlknf1oclwwlkn  30702  frgrncvvdeq  30937  avril1  31091  0vfval  31235  imsval  31314  imsdval  31315  bcseqi  31749  normpythi  31771  cm0  32238  fh1  32247  pjcji  32313  opsqrlem5  32773  pjsdi2i  32786  pjclem3  32826  pjci  32829  golem1  32900  iuneq12daf  33220  iunrdx  33227  ofresid  33305  cnvprop  33357  coprprop  33360  dp2eq1  33506  dp2eq2  33507  fzto1st1  33730  gsumvsca1  33854  gsumvsca2  33855  urpropd  33858  resv1r  33967  nsgqusf1olem2  34032  oppr2idl  34077  opprqus0g  34081  ressply1evls1  34164  esplyfvn  34276  vietalem  34278  lindsunlem  34323  fedgmullem1  34328  fedgmullem2  34329  fedgmul  34330  fldsdrgfldext2  34361  fldextrspunlem1  34374  fldextrspunfld  34375  algextdeglem4  34419  crefeq  34544  rspectopn  34566  xrge0mulc1cn  34640  qqhval2  34681  esumeq12dvaf  34730  esumeq2  34735  esumf1o  34749  esumfzf  34768  esumss  34771  esumpfinvalf  34775  ofceq  34796  carsgclctunlem1  35016  itgeq12dv  35025  ccatmulgnn0dir  35241  breprexpnat  35330  bnj956  35474  bnj1385  35529  bnj96  35562  bnj548  35594  bnj553  35595  bnj554  35596  bnj602  35612  bnj18eq1  35624  bnj1234  35710  bnj1296  35718  bnj1318  35722  bnj1442  35746  bnj1450  35747  cvmliftlem5  36220  cvmliftlem10  36225  cvmlift2lem9  36242  cvmliftphtlem  36248  satfdm  36300  mthmpps  36513  rdgprc  36733  dfrdg2  36734  wsuceq123  36753  wlimeq12  36758  altopthsn  36903  altxpeq1  36915  altxpeq2  36916  nmulprop  37116  ixpeq12dv  37182  prodeq12sdv  37184  itgeq12sdv  37185  ditgeq123dv  37187  cbvcsbdavw  37225  cbvcsbdavw2  37226  cbvrabdavw  37227  cbviundavw  37228  cbviindavw  37229  cbvopab1davw  37230  cbvopab2davw  37231  cbvopabdavw  37232  cbvmptdavw  37233  cbviotadavw  37235  cbvriotadavw  37236  cbvoprab1davw  37237  cbvoprab2davw  37238  cbvoprab3davw  37239  cbvoprab123davw  37240  cbvoprab12davw  37241  cbvoprab23davw  37242  cbvoprab13davw  37243  cbvixpdavw  37244  cbvsumdavw  37245  cbvproddavw  37246  cbvitgdavw  37247  cbvditgdavw  37248  cbvrabdavw2  37251  cbviundavw2  37252  cbviindavw2  37253  cbvmptdavw2  37254  cbvriotadavw2  37256  cbvmpodavw2  37257  cbvmpo1davw2  37258  cbvmpo2davw2  37259  cbvixpdavw2  37260  cbvsumdavw2  37261  cbvproddavw2  37262  cbvitgdavw2  37263  cbvditgdavw2  37264  ee7.2aOLD  37426  ttceq  37453  bj-sngleq  38057  bj-tageq  38066  bj-projeq  38082  bj-projval  38086  bj-1upleq  38089  bj-pr1eq  38092  bj-pr2eq  38106  bj-evaleq  38182  bj-imafv  38363  csbrecsg  38442  csbrdgg  38443  csboprabg  38444  csbmpo123  38445  finxpeq1  38500  finxpeq2  38501  csbfinxpg  38502  finxpreclem4  38508  unceq  38715  unccur  38717  finixpnum  38719  ptrest  38728  poimirlem3  38732  poimirlem9  38738  poimirlem15  38744  poimirlem16  38745  poimirlem26  38755  poimirlem27  38756  mbfposadd  38776  cnambfre  38777  iblabsnclem  38792  ftc1anclem1  38802  heiborlem4  38939  heiborlem6  38941  mpobi123f  39285  iineq12f  39287  mptbi12f  39289  eccnvepres  39409  xrneq1  39519  xrneq2  39522  shiftstableeq2  39606  cosseq  39639  redundss3  39835  riotaclbgBAD  40202  toycom  40221  ldualvbase  40374  ldualfvadd  40376  ldualsca  40380  ldualsbase  40381  ldualsaddN  40382  ldualfvs  40384  ldual0  40395  ldual1  40396  ldualneg  40397  cdleme19f  41556  cdleme20m  41571  cdleme21k  41586  cdleme27b  41616  cdleme31so  41627  cdleme31sn  41628  cdleme31se  41630  cdleme31se2  41631  cdleme31sc  41632  cdleme31sde  41633  cdleme31fv  41638  cdleme40v  41717  cdleme43dN  41740  cdlemeg46ngfr  41766  ltrnco4  41987  tgrpbase  41994  tgrpopr  41995  erngbase  42049  erngfplus  42050  erngfmul  42053  erngbase-rN  42057  erngfplus-rN  42058  erngfmul-rN  42061  dvasca  42254  dvavbase  42261  dvafvadd  42262  dvafvsca  42264  tendocnv  42269  dvhsca  42330  dvhfplusr  42332  dvhvbase  42335  dvhfvadd  42339  dvhfvsca  42348  lcdvadd  42845  lcdsbase  42848  lcdsadd  42849  lcdvs  42851  lcd0  42856  lcd1  42857  lcdneg  42858  fsuppind  43809  imaiinfv  43895  mapfzcons1  43919  rexrabdioph  43992  dnnumch1  44242  dnwech  44246  aomclem6  44252  pwssplit4  44282  pwfi2f1o  44289  mendplusgfval  44373  mendvscafval  44378  harval3  44729  dssmapntrcls  45318  colleq12d  45427  uzmptshftfval  45520  dropab1  45619  dropab2  45620  iineq12dv  46324  rabbida2  46350  rabbida3  46353  itgsinexplem1  47167  wallispi2lem2  47285  fourierdlem36  47356  etransclem4  47451  fcoreslem1  48336  afveq12d  48406  aoveq123d  48451  aovfundmoveq  48454  aovnuoveq  48464  aovvoveq  48465  aovovn0oveq  48467  afv2eq12d  48488  fsumsplitsndif  48654  rngccofvalALTV  49570  rhmsubcALTVlem2  49582  ringccofvalALTV  49604  itscnhlinecirc02plem2  50098  oppfrcl3  50449  oppf1st2nd  50450  uppropd  50500  natoppf  50554  catcrcl  50733  lmdpropd  51043  cmdpropd  51044  lmddu  51053  cmddu  51054  setrecseq  51066  aacllem  51217