Theorem 3eqtr4g 2669

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

Syntax hints:   → wi 4   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  rabbidva2  3162  rabeqf  3165  csbeq1  3502  csbeq2  3503  difeq1  3683  difeq2  3684  uneq2  3723  ineq2  3770  symdifeq1  3808  symdifeq2  3809  dfrab3ss  3864  csbprc  3932  csbeq2d  3943  csbnestgf  3948  disjssun  3988  ifeq1  4040  ifeq2  4041  pweq  4111  sneq  4135  csbsng  4190  csbprg  4191  rabsn  4200  preq1  4212  preq2  4213  tpeq1  4221  tpeq2  4222  tpeq3  4223  prprc1  4243  tpprceq3  4276  opeq1  4340  opeq2  4341  oteq1  4349  oteq2  4350  oteq3  4351  csbopg  4358  unieq  4380  csbuni  4402  inteq  4413  iineq1  4471  iineq2  4474  dfiin2g  4489  iinrab  4518  iinin1  4527  iinxprg  4537  iununi  4546  opabbid  4647  mpteq12f  4661  csbmpt12  4934  xpeq1  5052  xpeq2  5053  rneq  5272  reseq1  5311  reseq2  5312  resima2  5352  resindm  5364  resmpt  5369  imaeq1  5380  imaeq2  5381  mptcnv  5453  xpdisj1  5474  xpdisj2  5475  resdisj  5482  dmpropg  5526  rnpropg  5533  cores  5555  cores2  5565  xpco  5592  predeq123  5598  sspred  5605  suceq  5707  sucprc  5717  iotaeq  5776  iotabi  5777  fntpg  5862  imain  5888  f1oprswap  6092  fveq1  6102  fveq2  6103  fvres  6117  csbfv12  6141  fnimapr  6172  fvco2  6183  residpr  6315  fsnunfv  6358  fsnunres  6359  funiunfv  6410  fliftf  6465  isoini2  6489  riotaeqdv  6512  riotabidv  6513  riotauni  6517  riotabidva  6527  snriota  6540  oveq  6555  oveq1  6556  oveq2  6557  oprabbid  6606  mpt2eq123  6612  mpt2eq123dva  6614  mpt2eq3dva  6617  resmpt2  6656  ovres  6698  f1ocnvd  6782  ofeq  6797  ofreq  6798  fpar  7168  wrecseq123  7295  onovuni  7326  recseq  7357  tfr2a  7378  rdgeq1  7394  rdgeq2  7395  rdgsucmptf  7411  frsucmpt  7420  seqomeq12  7436  seqomsuc  7439  omopthi  7624  eceq1  7669  eceq2  7671  qseq1  7683  qseq2  7684  uniqs  7694  ecinxp  7709  qsinxp  7710  erovlem  7730  ecopovtrn  7737  ixpeq1  7805  supeq1  8234  supeq2  8237  supeq3  8238  supeq123d  8239  infeq1  8265  infeq2  8268  infeq3  8269  infeq123d  8270  infiso  8296  oieq1  8300  oieq2  8301  ordtypelem1  8306  inf3lemc  8406  wemapwe  8477  r1sucg  8515  r1limg  8517  rankprb  8597  karden  8641  cardiun  8691  acneq  8749  alephlim  8773  alephsuc  8774  alephfplem2  8811  infpssrlem2  9009  fin23lem34  9051  fin23lem35  9052  zorn2lem1  9201  zorn2lem7  9207  fpwwe2lem6  9336  fpwwe2lem13  9343  addpiord  9585  mulpiord  9586  addpqnq  9639  mulpqnq  9642  addassnq  9659  mulassnq  9660  distrnq  9662  lterpq  9671  ltexnq  9676  ltsrpr  9777  00sr  9799  recexsrlem  9803  mulgt0sr  9805  addcnsrec  9843  mulcnsrec  9844  negeq  10152  csbnegg  10157  negsubdi  10216  mulneg1  10345  negfi  10850  deceq1  11376  deceq1OLD  11377  deceq2  11378  deceq2OLD  11379  xnegeq  11912  fseq1p1m1  12283  om2uzrdg  12617  uzrdgsuci  12621  seqeq1  12666  seqeq2  12667  seqeq3  12668  seqfeq4  12712  seqof  12720  hashprg  13043  hashprgOLD  13044  hashmap  13082  hashtpg  13121  csbwrdg  13189  s1eq  13233  cats1co  13452  s2eqd  13459  s3eqd  13460  s4eqd  13461  s5eqd  13462  s6eqd  13463  s7eqd  13464  s8eqd  13465  xpcogend  13561  shftval  13662  limsupgle  14056  lo1eq  14147  rlimeq  14148  sumeq1  14267  sumeq2w  14270  sumeq2ii  14271  zsum  14296  sumss2  14304  fsumsplitsnun  14328  isumclim3  14332  fsumcom2  14347  fsumcom2OLD  14348  incexclem  14407  incexc2  14409  isumshft  14410  prodeq1f  14477  prodeq2w  14481  prodeq2ii  14482  zprod  14506  fprodm1s  14539  fprodp1s  14540  fprodcom2  14553  fprodcom2OLD  14554  iprodclim3  14570  ef0lem  14648  ruclem7  14804  sadcp1  15015  smupp1  15040  smueqlem  15050  algrp1  15125  dfphi2  15317  prmdiveq  15329  pceulem  15388  vdwlem6  15528  cshwsiun  15644  setsid  15742  elbasfv  15748  elbasov  15749  imastset  16005  imasvscaval  16021  xpscg  16041  isoval  16248  funcoppc  16358  fulloppc  16405  fuccofval  16442  natpropd  16459  catccofval  16573  xpchomfval  16642  xpccofval  16645  lubfval  16801  glbfval  16814  grpidpropd  17084  gsumpropd2lem  17096  frmdplusg  17214  grpinvpropd  17313  grpsubpropd  17343  grpsubpropd2  17344  mulgpropd  17407  oppgmnd  17607  symgplusg  17632  sylow1lem2  17837  sylow3lem1  17865  prds1  18437  pwsmgp  18441  opprring  18454  rngidpropd  18518  dvdsrpropd  18519  unitpropd  18520  invrpropd  18521  rhm1  18553  lmhmpropd  18894  lidlrsppropd  19051  lpival  19066  ressascl  19165  asclpropd  19167  aspval2  19168  psrbas  19199  psrplusg  19202  psrmulr  19205  psrvscafval  19211  resspsrbas  19236  ressmplbas2  19276  opsrle  19296  opsrbaslem  19298  opsrbaslemOLD  19299  vr1val  19383  ressply1add  19421  ressply1mul  19422  ressply1vsca  19423  psrplusgpropd  19427  mplbaspropd  19428  psropprmul  19429  ply1baspropd  19434  ply1plusgpropd  19435  ply1sca2  19445  subrgvr1  19452  coe1mul2lem2  19459  ply1coe1eq  19489  zrhpropd  19682  znle  19703  frlmplusgval  19926  frlmvscafval  19928  mamudi  20028  mamudir  20029  matrcl  20037  oftpos  20077  mattpos1  20081  mdetfval  20211  mdetrlin  20227  mdetrsca  20228  mdetrsca2  20229  mdetrlin2  20232  mdetunilem5  20241  madufval  20262  madugsum  20268  idmatidpmat  20361  cpmidpmat  20497  cncmp  21005  2ndcsep  21072  llyeq  21083  nllyeq  21084  xkouni  21212  hmphindis  21410  xkocnv  21427  ptcmplem2  21667  snclseqg  21729  prdstmdd  21737  ustexsym  21829  ucnextcn  21918  metreslem  21977  comet  22128  nrmmetd  22189  nmpropd  22208  isngp3  22212  ngpds  22218  subgnm  22247  tngnm  22265  idnghm  22357  cnmetdval  22384  cnmpt2pc  22535  htpyco2  22586  phtpyco2  22597  clsocv  22857  rrxprds  22985  rrxnm  22987  ovolunlem1a  23071  voliunlem3  23127  ioombl1lem4  23136  uniioombllem4  23160  itg11  23264  itgeq1f  23344  itgeq2  23350  iblss2  23378  itgss  23384  itgeqa  23386  itgfsum  23399  itgsplit  23408  ditgeq1  23418  ditgeq2  23419  ditgeq3  23420  dvcmulf  23514  dvmptfsum  23542  dvcnvrelem2  23585  mdegfval  23626  mdegpropd  23648  deg1propd  23650  plyeq0  23771  coe11  23813  dgrlt  23826  dgradd2  23828  dgrmulc  23831  dvply1  23843  fta1lem  23866  pserulm  23980  rlimcnp2  24493  jensenlem1  24513  basellem5  24611  dchrbas  24760  dchrrcl  24765  dchrplusg  24772  dchrfi  24780  lgsdi  24859  lgseisenlem2  24901  lgsquadlem3  24907  dchrmusumlema  24982  rpvmasum2  25001  dchrisum0lema  25003  pntlemg  25087  colperpexlem2  25423  axlowdimlem13  25634  uhgrvtxedgiedgb  25810  nbgraf1olem5  25974  nb3graprlem1  25980  constr2spthlem1  26124  constr3pthlem1  26183  constr3pthlem2  26184  avril1  26711  0vfval  26845  imsval  26924  imsdval  26925  bcseqi  27361  normpythi  27383  cm0  27852  fh1  27861  pjcji  27927  opsqrlem5  28387  pjsdi2i  28400  pjclem3  28440  pjci  28443  golem1  28514  iunrdx  28764  ofresid  28824  mpteq12df  28837  resmptf  28838  f1od2  28887  gsumvsca1  29113  gsumvsca2  29114  rhmopp  29150  resv1r  29168  fzto1st1  29183  crefeq  29240  xrge0mulc1cn  29315  qqhval2  29354  esumeq12dvaf  29420  esumeq2  29425  esumf1o  29439  esumfzf  29458  esumss  29461  esumpfinvalf  29465  ofceq  29486  carsgclctunlem1  29706  itgeq12dv  29715  ccatmulgnn0dir  29945  bnj956  30101  bnj1385  30157  bnj96  30189  bnj548  30221  bnj553  30222  bnj554  30223  bnj602  30239  bnj18eq1  30251  bnj1234  30335  bnj1296  30343  bnj1318  30347  bnj1442  30371  bnj1450  30372  cvmliftlem5  30525  cvmliftlem10  30530  cvmlift2lem9  30547  cvmliftphtlem  30553  mthmpps  30733  mpteq12d  30915  rdgprc  30944  dfrdg2  30945  trpredeq1  30964  trpredeq2  30965  trpredeq3  30966  wsuceq123  31004  wlimeq12  31009  altopthsn  31238  altxpeq1  31250  altxpeq2  31251  ee7.2aOLD  31630  bj-rabbida2  32105  bj-sngleq  32148  bj-tageq  32157  bj-projeq  32173  bj-projval  32177  bj-1upleq  32180  bj-pr1eq  32183  bj-pr2eq  32197  csbpredg  32348  csbwrecsg  32349  csbrecsg  32350  csbrdgg  32351  csboprabg  32352  csbmpt22g  32353  finxpeq1  32399  finxpeq2  32400  csbfinxpg  32401  finxpreclem4  32407  cureq  32555  unceq  32556  uncov  32560  unccur  32562  finixpnum  32564  ptrest  32578  poimirlem3  32582  poimirlem9  32588  poimirlem15  32594  poimirlem16  32595  poimirlem26  32605  poimirlem27  32606  mbfposadd  32627  cnambfre  32628  iblabsnclem  32643  ftc1anclem1  32655  heiborlem4  32783  heiborlem6  32785  mpt2bi123f  33141  iineq12f  33143  mptbi12f  33145  riotaclbgBAD  33258  toycom  33278  ldualvbase  33431  ldualfvadd  33433  ldualsca  33437  ldualsbase  33438  ldualsaddN  33439  ldualfvs  33441  ldual0  33452  ldual1  33453  ldualneg  33454  cdleme19f  34614  cdleme20m  34629  cdleme21k  34644  cdleme27b  34674  cdleme31so  34685  cdleme31sn  34686  cdleme31se  34688  cdleme31se2  34689  cdleme31sc  34690  cdleme31sde  34691  cdleme31fv  34696  cdleme40v  34775  cdleme43dN  34798  cdlemeg46ngfr  34824  ltrnco4  35045  tgrpbase  35052  tgrpopr  35053  erngbase  35107  erngfplus  35108  erngfmul  35111  erngbase-rN  35115  erngfplus-rN  35116  erngfmul-rN  35119  dvasca  35312  dvavbase  35319  dvafvadd  35320  dvafvsca  35322  tendocnv  35328  dvhsca  35389  dvhfplusr  35391  dvhvbase  35394  dvhfvadd  35398  dvhfvsca  35407  lcdvadd  35904  lcdsbase  35907  lcdsadd  35908  lcdvs  35910  lcd0  35915  lcd1  35916  lcdneg  35917  imaiinfv  36274  mapfzcons1  36298  rexrabdioph  36376  dnnumch1  36632  dnwech  36636  aomclem6  36647  pwssplit4  36677  pwfi2f1o  36684  mendplusgfval  36774  mendvscafval  36779  dssmapntrcls  37446  uzmptshftfval  37567  dropab1  37672  dropab2  37673  csbunigOLD  38073  csbfv12gALTOLD  38074  csbxpgOLD  38075  csbresgOLD  38077  csbrngOLD  38078  csbima12gALTOLD  38079  itgsinexplem1  38845  wallispi2lem2  38965  fourierdlem36  39036  etransclem4  39131  afveq12d  39862  aoveq123d  39907  aovfundmoveq  39910  aovnuoveq  39920  aovvoveq  39921  aovovn0oveq  39923  resisresindm  40320  fsumsplitsndif  40372  nb3grprlem1  40608  crctcshlem2  41021  frgrncvvdeq  41480  rngccofvalALTV  41779  ringccofvalALTV  41842  rhmsubclem2  41879  rhmsubcALTVlem2  41898  xpprsng  41903  setrecseq  42231  aacllem  42356