Theorem 3eqtr4g 2881

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	syl5eq 2868	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	syl6eqr 2874	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  rabbidva2  3476  rabeqf  3481  rabeqi  3482  csbeq1  3886  csbeq2  3888  csbeq2d  3889  difeq1  4092  difeq2  4093  uneq2  4133  ineq1  4181  ineq2  4183  symdifeq1  4221  symdifeq2  4222  dfrab3ss  4281  csbprc  4358  csbnestgfw  4371  csbnestgf  4376  disjssun  4417  ifeq1  4471  ifeq2  4472  pweqALT  4556  sneq  4577  csbsng  4644  csbprg  4645  preq1  4669  preq2  4670  tpeq1  4678  tpeq2  4679  tpeq3  4680  prprc1  4701  tpprceq3  4737  opeq1  4803  opeq2  4804  oteq1  4812  oteq2  4813  oteq3  4814  csbopg  4821  unieqOLD  4850  csbuni  4867  inteq  4879  iineq1  4936  iineq2  4939  iuneq12df  4945  dfiin2g  4957  iinrab  4991  iinin1  5001  iinxprg  5011  iununi  5021  opabbid  5131  mpteq12df  5148  mpteq12f  5149  csbmpt12  5444  xpeq1  5569  xpeq2  5576  rneq  5806  reseq1  5847  reseq2  5848  resima2  5888  resindm  5900  resmpt  5905  resmptf  5907  imaeq1  5924  imaeq2  5925  mptcnv  5998  xpdisj1  6018  xpdisj2  6019  resdisj  6026  dmpropg  6072  rnpropg  6079  cores  6102  cores2  6112  xpco  6140  predeq123  6149  sspred  6156  suceq  6256  sucprc  6266  iotaeq  6326  iotabi  6327  fntpg  6414  imain  6439  f1oprswap  6658  fveq1  6669  fveq2  6670  fvres  6689  csbfv12  6713  fnimapr  6747  fvco2  6758  xpprsng  6902  residpr  6905  fsnunfv  6949  fsnunres  6950  funiunfv  7007  fliftf  7068  isoini2  7092  riotaeqdv  7115  riotabidv  7116  riotauni  7120  riotabidva  7133  snriota  7147  oveq  7162  oveq1  7163  oveq2  7164  oprabbid  7219  mpoeq123  7226  mpoeq123dva  7228  mpoeq3dva  7231  resmpo  7272  ovres  7314  f1ocnvd  7396  ofeq  7411  ofreq  7412  fpar  7811  wrecseq123  7948  onovuni  7979  recseq  8010  tfr2a  8031  rdgeq1  8047  rdgeq2  8048  rdgsucmptf  8064  frsucmpt  8073  seqomeq12  8090  seqomsuc  8093  omopthi  8284  eceq1  8327  eceq2  8329  qseq1  8343  qseq2  8344  uniqs  8357  ecinxp  8372  qsinxp  8373  erovlem  8393  ecopovtrn  8400  ixpeq1  8472  supeq1  8909  supeq2  8912  supeq3  8913  supeq123d  8914  infeq1  8940  infeq2  8943  infeq3  8944  infeq123d  8945  infiso  8972  oieq1  8976  oieq2  8977  ordtypelem1  8982  inf3lemc  9089  wemapwe  9160  r1sucg  9198  r1limg  9200  rankprb  9280  karden  9324  djueq12  9333  cardiun  9411  acneq  9469  alephlim  9493  alephsuc  9494  alephfplem2  9531  infpssrlem2  9726  fin23lem34  9768  fin23lem35  9769  zorn2lem1  9918  zorn2lem7  9924  fpwwe2lem6  10057  fpwwe2lem13  10064  addpiord  10306  mulpiord  10307  addpqnq  10360  mulpqnq  10363  addassnq  10380  mulassnq  10381  distrnq  10383  lterpq  10392  ltexnq  10397  ltsrpr  10499  00sr  10521  recexsrlem  10525  mulgt0sr  10527  addcnsrec  10565  mulcnsrec  10566  negeq  10878  csbnegg  10883  negsubdi  10942  mulneg1  11076  negfi  11589  deceq1  12104  deceq2  12105  xnegeq  12601  fseq1p1m1  12982  om2uzrdg  13325  uzrdgsuci  13329  seqeq1  13373  seqeq2  13374  seqeq3  13375  seqfeq4  13420  seqof  13428  hashprg  13757  hashtpg  13844  csbwrdg  13895  s1eq  13954  cats1co  14218  s2eqd  14225  s3eqd  14226  s4eqd  14227  s5eqd  14228  s6eqd  14229  s7eqd  14230  s8eqd  14231  xpcogend  14334  shftval  14433  limsupgle  14834  lo1eq  14925  rlimeq  14926  sumeq1  15045  sumeq2w  15049  sumeq2ii  15050  zsum  15075  sumss2  15083  fsumsplitsnun  15110  isumclim3  15114  fsumcom2  15129  incexclem  15191  incexc2  15193  isumshft  15194  prodeq1f  15262  prodeq2w  15266  prodeq2ii  15267  zprod  15291  fprodm1s  15324  fprodp1s  15325  fprodcom2  15338  fprodsplitf  15342  iprodclim3  15354  ef0lem  15432  ruclem7  15589  sadcp1  15804  smupp1  15829  smueqlem  15839  algrp1  15918  dfphi2  16111  prmdiveq  16123  pceulem  16182  vdwlem6  16322  cshwsiun  16433  sloteq  16488  setsid  16538  elbasfv  16544  elbasov  16545  imastset  16795  imasvscaval  16811  isoval  17035  funcoppc  17145  fulloppc  17192  fuccofval  17229  natpropd  17246  catccofval  17360  xpchomfval  17429  xpccofval  17432  lubfval  17588  glbfval  17601  grpidpropd  17872  gsumpropd2lem  17889  frmdplusg  18019  efmndplusg  18045  grpinvpropd  18174  grpsubpropd  18204  grpsubpropd2  18205  mulgpropd  18269  oppgmnd  18482  sylow1lem2  18724  sylow3lem1  18752  prds1  19364  pwsmgp  19368  opprring  19381  rngidpropd  19445  dvdsrpropd  19446  unitpropd  19447  invrpropd  19448  rhm1  19482  lmhmpropd  19845  lidlrsppropd  20003  lpival  20018  ressascl  20125  asclpropd  20126  aspval2  20127  psrbas  20158  psrplusg  20161  psrmulr  20164  psrvscafval  20170  resspsrbas  20195  ressmplbas2  20236  opsrle  20256  opsrbaslem  20258  vr1val  20360  ressply1add  20398  ressply1mul  20399  ressply1vsca  20400  psrplusgpropd  20404  mplbaspropd  20405  psropprmul  20406  ply1baspropd  20411  ply1plusgpropd  20412  ply1sca2  20422  subrgvr1  20429  coe1mul2lem2  20436  ply1coe1eq  20466  zrhpropd  20662  znle  20683  frlmplusgval  20908  frlmvscafval  20910  mamudi  21012  mamudir  21013  matrcl  21021  oftpos  21061  mattpos1  21065  mdetfval  21195  mdetrlin  21211  mdetrsca  21212  mdetrsca2  21213  mdetrlin2  21216  mdetunilem5  21225  madufval  21246  madugsum  21252  idmatidpmat  21345  cpmidpmat  21481  cncmp  22000  2ndcsep  22067  llyeq  22078  nllyeq  22079  xkouni  22207  hmphindis  22405  xkocnv  22422  ptcmplem2  22661  snclseqg  22724  prdstmdd  22732  ustexsym  22824  ucnextcn  22913  metreslem  22972  comet  23123  nrmmetd  23184  nmpropd  23203  isngp3  23207  ngpds  23213  subgnm  23242  tngnm  23260  idnghm  23352  cnmetdval  23379  cnmpopc  23532  htpyco2  23583  phtpyco2  23594  clsocv  23853  rrxprds  23992  rrxnm  23994  rrxplusgvscavalb  23998  ovolunlem1a  24097  voliunlem3  24153  ioombl1lem4  24162  uniioombllem4  24187  itg11  24292  itgeq1f  24372  itgeq2  24378  iblss2  24406  itgss  24412  itgeqa  24414  itgfsum  24427  itgsplit  24436  ditgeq1  24446  ditgeq2  24447  ditgeq3  24448  dvcmulf  24542  dvmptfsum  24572  dvcnvrelem2  24615  mdegfval  24656  mdegpropd  24678  deg1propd  24680  plyeq0  24801  coe11  24843  dgrlt  24856  dgradd2  24858  dgrmulc  24861  dvply1  24873  fta1lem  24896  pserulm  25010  rlimcnp2  25544  jensenlem1  25564  basellem5  25662  dchrbas  25811  dchrrcl  25816  dchrplusg  25823  dchrfi  25831  lgsdi  25910  lgseisenlem2  25952  lgsquadlem3  25958  dchrmusumlema  26069  rpvmasum2  26088  dchrisum0lema  26090  pntlemg  26174  colperpexlem2  26517  axlowdimlem13  26740  uhgrvtxedgiedgb  26921  nb3grprlem1  27162  crctcshlem2  27596  wpthswwlks2on  27740  clwlknf1oclwwlkn  27863  frgrncvvdeq  28088  avril1  28242  0vfval  28383  imsval  28462  imsdval  28463  bcseqi  28897  normpythi  28919  cm0  29386  fh1  29395  pjcji  29461  opsqrlem5  29921  pjsdi2i  29934  pjclem3  29974  pjci  29977  golem1  30048  iuneq12daf  30308  iunrdx  30315  ofresid  30389  fnimatp  30423  cnvprop  30432  coprprop  30435  f1od2  30457  dp2eq1  30549  dp2eq2  30550  fzto1st1  30744  gsumvsca1  30854  gsumvsca2  30855  rhmopp  30892  resv1r  30910  lindsunlem  31020  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  crefeq  31109  xrge0mulc1cn  31184  qqhval2  31223  esumeq12dvaf  31290  esumeq2  31295  esumf1o  31309  esumfzf  31328  esumss  31331  esumpfinvalf  31335  ofceq  31356  carsgclctunlem1  31575  itgeq12dv  31584  ccatmulgnn0dir  31812  breprexpnat  31905  bnj956  32048  bnj1385  32104  bnj96  32137  bnj548  32169  bnj553  32170  bnj554  32171  bnj602  32187  bnj18eq1  32199  bnj1234  32285  bnj1296  32293  bnj1318  32297  bnj1442  32321  bnj1450  32322  cvmliftlem5  32536  cvmliftlem10  32541  cvmlift2lem9  32558  cvmliftphtlem  32564  satfdm  32616  mthmpps  32829  eqfunressuc  33005  rdgprc  33039  dfrdg2  33040  trpredeq1  33059  trpredeq2  33060  trpredeq3  33061  wsuceq123  33101  wlimeq12  33106  frecseq123  33119  nosupbnd2lem1  33215  altopthsn  33422  altxpeq1  33434  altxpeq2  33435  ee7.2aOLD  33809  bj-rabbida2  34240  bj-sngleq  34282  bj-tageq  34291  bj-projeq  34307  bj-projval  34311  bj-1upleq  34314  bj-pr1eq  34317  bj-pr2eq  34331  bj-evaleq  34366  bj-imafv  34536  bj-isrvec  34578  csbpredg  34610  csbwrecsg  34611  csbrecsg  34612  csbrdgg  34613  csboprabg  34614  csbmpo123  34615  finxpeq1  34670  finxpeq2  34671  csbfinxpg  34672  finxpreclem4  34678  cureq  34883  unceq  34884  uncov  34888  unccur  34890  finixpnum  34892  ptrest  34906  poimirlem3  34910  poimirlem9  34916  poimirlem15  34922  poimirlem16  34923  poimirlem26  34933  poimirlem27  34934  mbfposadd  34954  cnambfre  34955  iblabsnclem  34970  ftc1anclem1  34982  heiborlem4  35107  heiborlem6  35109  mpobi123f  35455  iineq12f  35457  mptbi12f  35459  eccnvepres  35552  uniqsALTV  35601  xrneq1  35644  xrneq2  35647  cosseq  35686  redundss3  35878  riotaclbgBAD  36105  toycom  36124  ldualvbase  36277  ldualfvadd  36279  ldualsca  36283  ldualsbase  36284  ldualsaddN  36285  ldualfvs  36287  ldual0  36298  ldual1  36299  ldualneg  36300  cdleme19f  37459  cdleme20m  37474  cdleme21k  37489  cdleme27b  37519  cdleme31so  37530  cdleme31sn  37531  cdleme31se  37533  cdleme31se2  37534  cdleme31sc  37535  cdleme31sde  37536  cdleme31fv  37541  cdleme40v  37620  cdleme43dN  37643  cdlemeg46ngfr  37669  ltrnco4  37890  tgrpbase  37897  tgrpopr  37898  erngbase  37952  erngfplus  37953  erngfmul  37956  erngbase-rN  37960  erngfplus-rN  37961  erngfmul-rN  37964  dvasca  38157  dvavbase  38164  dvafvadd  38165  dvafvsca  38167  tendocnv  38172  dvhsca  38233  dvhfplusr  38235  dvhvbase  38238  dvhfvadd  38242  dvhfvsca  38251  lcdvadd  38748  lcdsbase  38751  lcdsadd  38752  lcdvs  38754  lcd0  38759  lcd1  38760  lcdneg  38761  prjspnval2  39316  imaiinfv  39339  mapfzcons1  39363  rexrabdioph  39440  dnnumch1  39693  dnwech  39697  aomclem6  39708  pwssplit4  39738  pwfi2f1o  39745  mendplusgfval  39834  mendvscafval  39839  harval3  39953  dssmapntrcls  40527  scotteqd  40622  colleq12d  40638  uzmptshftfval  40727  dropab1  40828  dropab2  40829  rabbida2  41448  rabbida3  41451  itgsinexplem1  42288  wallispi2lem2  42406  fourierdlem36  42477  etransclem4  42572  afveq12d  43381  aoveq123d  43426  aovfundmoveq  43429  aovnuoveq  43439  aovvoveq  43440  aovovn0oveq  43442  afv2eq12d  43463  fsumsplitsndif  43582  rngccofvalALTV  44307  ringccofvalALTV  44370  rhmsubclem2  44407  rhmsubcALTVlem2  44425  itscnhlinecirc02plem2  44819  setrecseq  44837  aacllem  44951