Theorem 3eqtr4g 2802

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

Syntax hints:   → wi 4   = wceq 1540

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2729

This theorem is referenced by:  rabbidva2  3406  rabeqf  3434  rabeqiOLD  3438  csbeq1  3844  csbeq2  3846  csbeq2d  3847  difeq1  4060  difeq2  4061  uneq2  4101  ineq1  4149  ineq2  4150  symdifeq1  4188  symdifeq2  4189  dfrab3ss  4256  csbprc  4350  csbnestgfw  4363  csbnestgf  4368  disjssun  4411  ifeq1  4473  ifeq2  4474  pweqALT  4558  sneq  4579  csbsng  4652  csbprg  4653  preq1  4677  preq2  4678  tpeq1  4686  tpeq2  4687  tpeq3  4688  prprc1  4709  tpprceq3  4747  opeq1  4813  opeq2  4814  oteq1  4822  oteq2  4823  oteq3  4824  csbopg  4831  unieqOLD  4860  uniprg  4865  csbuni  4880  inteq  4893  iineq1  4952  iineq2  4955  iuneq12df  4961  dfiin2g  4973  iinrab  5009  iinin1  5019  iinxprg  5029  iununi  5039  opabbid  5150  opabbidv  5151  mpteq12da  5170  mpteq12dfOLD  5172  mpteq12f  5173  mpteq12dva  5174  csbmpt12  5488  xpeq1  5619  xpeq2  5626  rneq  5862  reseq1  5902  reseq2  5903  resima2  5943  resindm  5957  resmpt  5962  resmptf  5964  imaeq1  5979  imaeq2  5980  mptcnv  6063  xpdisj1  6084  xpdisj2  6085  resdisj  6092  dmpropg  6138  rnpropg  6145  cores  6172  cores2  6182  xpco  6212  predeq123  6223  csbpredg  6228  sspred  6231  predres  6262  suceq  6351  sucprc  6361  iotaeq  6428  iotabi  6429  fntpg  6528  imain  6553  f1oprswap  6795  fveq1  6808  fveq2  6809  fvres  6828  csbfv12  6854  fnimapr  6889  fvco2  6902  xpprsng  7049  residpr  7052  fsnunfv  7096  fsnunres  7097  funiunfv  7158  f1ofvswap  7215  fliftf  7223  isoini2  7247  riotaeqdv  7271  riotabidv  7272  riotauni  7276  riotabidva  7290  snriota  7304  oveq  7319  oveq1  7320  oveq2  7321  oprabbid  7378  oprabbidv  7379  mpoeq123  7385  mpoeq123dva  7387  mpoeq3dva  7390  resmpo  7432  ovres  7476  f1ocnvd  7558  ofeqd  7573  ofreq  7575  fpar  7999  frecseq123  8143  csbfrecsg  8145  wrecseq123  8175  wrecseq123OLD  8176  csbwrecsg  8182  onovuni  8218  recseq  8250  tfr2a  8271  rdgeq1  8287  rdgeq2  8288  rdgsucmptf  8304  frsucmpt  8314  seqomeq12  8330  seqomsuc  8333  omopthi  8537  eceq1  8582  eceq2  8584  qseq1  8598  qseq2  8599  uniqs  8612  ecinxp  8627  qsinxp  8628  erovlem  8648  ecopovtrn  8655  ixpeq1  8742  unfi  9012  supeq1  9272  supeq2  9275  supeq3  9276  supeq123d  9277  infeq1  9303  infeq2  9306  infeq3  9307  infeq123d  9308  infiso  9335  oieq1  9339  oieq2  9340  ordtypelem1  9345  inf3lemc  9452  wemapwe  9523  ttrcleq  9535  r1sucg  9595  r1limg  9597  rankprb  9677  karden  9721  djueq12  9730  cardiun  9808  acneq  9869  alephlim  9893  alephsuc  9894  alephfplem2  9931  infpssrlem2  10130  fin23lem34  10172  fin23lem35  10173  zorn2lem1  10322  zorn2lem7  10328  fpwwe2lem5  10461  fpwwe2lem12  10468  addpiord  10710  mulpiord  10711  addpqnq  10764  mulpqnq  10767  addassnq  10784  mulassnq  10785  distrnq  10787  lterpq  10796  ltexnq  10801  ltsrpr  10903  00sr  10925  recexsrlem  10929  mulgt0sr  10931  addcnsrec  10969  mulcnsrec  10970  negeq  11283  csbnegg  11288  negsubdi  11347  mulneg1  11481  negfi  11994  deceq1  12512  deceq2  12513  xnegeq  13011  fseq1p1m1  13400  om2uzrdg  13746  uzrdgsuci  13750  seqeq1  13794  seqeq2  13795  seqeq3  13796  seqfeq4  13842  seqof  13850  hashprg  14179  hashtpg  14268  csbwrdg  14316  s1eq  14374  cats1co  14638  s2eqd  14645  s3eqd  14646  s4eqd  14647  s5eqd  14648  s6eqd  14649  s7eqd  14650  s8eqd  14651  xpcogend  14754  shftval  14854  limsupgle  15255  lo1eq  15346  rlimeq  15347  sumeq1  15469  sumeq2w  15473  sumeq2ii  15474  zsum  15499  sumss2  15507  fsumsplitsnun  15536  isumclim3  15540  fsumcom2  15555  incexclem  15617  incexc2  15619  isumshft  15620  prodeq1f  15687  prodeq2w  15691  prodeq2ii  15692  zprod  15716  fprodm1s  15749  fprodp1s  15750  fprodcom2  15763  fprodsplitf  15767  iprodclim3  15779  ef0lem  15857  ruclem7  16014  sadcp1  16231  smupp1  16256  smueqlem  16266  algrp1  16346  dfphi2  16542  prmdiveq  16554  pceulem  16613  vdwlem6  16754  cshwsiun  16868  sloteq  16951  setsid  16976  elbasfv  16985  elbasov  16986  imastset  17300  imasvscaval  17316  isoval  17544  funcoppc  17657  fulloppc  17705  fuccofval  17743  natpropd  17761  catccofval  17886  xpchomfval  17963  xpccofval  17966  lubfval  18135  glbfval  18148  grpidpropd  18413  gsumpropd2lem  18430  frmdplusg  18560  efmndplusg  18586  grpinvpropd  18717  grpsubpropd  18747  grpsubpropd2  18748  mulgpropd  18812  oppgmnd  19028  sylow1lem2  19271  sylow3lem1  19299  prds1  19920  pwsmgp  19924  opprring  19940  rngidpropd  20004  dvdsrpropd  20005  unitpropd  20006  invrpropd  20007  rhm1  20041  rhmopp  20059  lmhmpropd  20406  lidlrsppropd  20572  lpival  20587  zrhpropd  20787  znle  20811  frlmplusgval  21042  frlmvscafval  21044  ressascl  21171  asclpropd  21172  aspval2  21173  psrbas  21218  psrplusg  21221  psrmulr  21224  psrvscafval  21230  resspsrbas  21255  ressmplbas2  21299  opsrle  21319  opsrbaslem  21321  opsrbaslemOLD  21322  vr1val  21434  ressply1add  21472  ressply1mul  21473  ressply1vsca  21474  psrplusgpropd  21478  mplbaspropd  21479  psropprmul  21480  ply1baspropd  21485  ply1plusgpropd  21486  ply1sca2  21496  subrgvr1  21503  coe1mul2lem2  21510  ply1coe1eq  21540  mamudi  21621  mamudir  21622  matrcl  21630  oftpos  21672  mattpos1  21676  mdetfval  21806  mdetrlin  21822  mdetrsca  21823  mdetrsca2  21824  mdetrlin2  21827  mdetunilem5  21836  madufval  21857  madugsum  21863  idmatidpmat  21957  cpmidpmat  22093  cncmp  22614  2ndcsep  22681  llyeq  22692  nllyeq  22693  xkouni  22821  hmphindis  23019  xkocnv  23036  ptcmplem2  23275  snclseqg  23338  prdstmdd  23346  ustexsym  23438  ucnextcn  23527  metreslem  23586  comet  23740  nrmmetd  23801  nmpropd  23821  isngp3  23825  ngpds  23831  subgnm  23860  tngnm  23886  idnghm  23978  cnmetdval  24005  cnmpopc  24162  htpyco2  24213  phtpyco2  24224  clsocv  24485  rrxprds  24624  rrxnm  24626  rrxplusgvscavalb  24630  ovolunlem1a  24731  voliunlem3  24787  ioombl1lem4  24796  uniioombllem4  24821  itg11  24926  itgeq1f  25007  itgeq2  25013  iblss2  25041  itgss  25047  itgeqa  25049  itgfsum  25062  itgsplit  25071  ditgeq1  25083  ditgeq2  25084  ditgeq3  25085  dvcmulf  25180  dvmptfsum  25210  dvcnvrelem2  25253  mdegfval  25298  mdegpropd  25320  deg1propd  25322  plyeq0  25443  coe11  25485  dgrlt  25498  dgradd2  25500  dgrmulc  25503  dvply1  25515  fta1lem  25538  pserulm  25652  rlimcnp2  26187  jensenlem1  26207  basellem5  26305  dchrbas  26454  dchrrcl  26459  dchrplusg  26466  dchrfi  26474  lgsdi  26553  lgseisenlem2  26595  lgsquadlem3  26601  dchrmusumlema  26712  rpvmasum2  26731  dchrisum0lema  26733  pntlemg  26817  colperpexlem2  27200  axlowdimlem13  27430  uhgrvtxedgiedgb  27614  nb3grprlem1  27855  crctcshlem2  28291  wpthswwlks2on  28434  clwlknf1oclwwlkn  28556  frgrncvvdeq  28781  avril1  28935  0vfval  29076  imsval  29155  imsdval  29156  bcseqi  29590  normpythi  29612  cm0  30079  fh1  30088  pjcji  30154  opsqrlem5  30614  pjsdi2i  30627  pjclem3  30667  pjci  30670  golem1  30741  iuneq12daf  31004  iunrdx  31011  ofresid  31087  fnimatp  31122  cnvprop  31137  coprprop  31140  f1od2  31164  dp2eq1  31255  dp2eq2  31256  fzto1st1  31477  gsumvsca1  31587  gsumvsca2  31588  resv1r  31645  nsgqusf1olem2  31704  lindsunlem  31811  fedgmullem1  31816  fedgmullem2  31817  fedgmul  31818  crefeq  31901  rspectopn  31923  xrge0mulc1cn  31997  qqhval2  32038  esumeq12dvaf  32105  esumeq2  32110  esumf1o  32124  esumfzf  32143  esumss  32146  esumpfinvalf  32150  ofceq  32171  carsgclctunlem1  32390  itgeq12dv  32399  ccatmulgnn0dir  32627  breprexpnat  32720  bnj956  32862  bnj1385  32918  bnj96  32951  bnj548  32983  bnj553  32984  bnj554  32985  bnj602  33001  bnj18eq1  33013  bnj1234  33099  bnj1296  33107  bnj1318  33111  bnj1442  33135  bnj1450  33136  cvmliftlem5  33357  cvmliftlem10  33362  cvmlift2lem9  33379  cvmliftphtlem  33385  satfdm  33437  mthmpps  33650  eqfunressuc  33839  rdgprc  33872  dfrdg2  33873  wsuceq123  33906  wlimeq12  33911  nosupbnd2lem1  33979  lruneq  34147  addsval  34187  altopthsn  34324  altxpeq1  34336  altxpeq2  34337  ee7.2aOLD  34711  bj-rabbida2  35166  bj-sngleq  35217  bj-tageq  35226  bj-projeq  35242  bj-projval  35246  bj-1upleq  35249  bj-pr1eq  35252  bj-pr2eq  35266  bj-evaleq  35303  bj-imafv  35482  csbrecsg  35559  csbrdgg  35560  csboprabg  35561  csbmpo123  35562  finxpeq1  35617  finxpeq2  35618  csbfinxpg  35619  finxpreclem4  35625  cureq  35813  unceq  35814  uncov  35818  unccur  35820  finixpnum  35822  ptrest  35836  poimirlem3  35840  poimirlem9  35846  poimirlem15  35852  poimirlem16  35853  poimirlem26  35863  poimirlem27  35864  mbfposadd  35884  cnambfre  35885  iblabsnclem  35900  ftc1anclem1  35910  heiborlem4  36032  heiborlem6  36034  mpobi123f  36380  iineq12f  36382  mptbi12f  36384  eccnvepres  36502  uniqsALTV  36554  xrneq1  36603  xrneq2  36606  cosseq  36652  redundss3  36854  riotaclbgBAD  37180  toycom  37199  ldualvbase  37352  ldualfvadd  37354  ldualsca  37358  ldualsbase  37359  ldualsaddN  37360  ldualfvs  37362  ldual0  37373  ldual1  37374  ldualneg  37375  cdleme19f  38534  cdleme20m  38549  cdleme21k  38564  cdleme27b  38594  cdleme31so  38605  cdleme31sn  38606  cdleme31se  38608  cdleme31se2  38609  cdleme31sc  38610  cdleme31sde  38611  cdleme31fv  38616  cdleme40v  38695  cdleme43dN  38718  cdlemeg46ngfr  38744  ltrnco4  38965  tgrpbase  38972  tgrpopr  38973  erngbase  39027  erngfplus  39028  erngfmul  39031  erngbase-rN  39035  erngfplus-rN  39036  erngfmul-rN  39039  dvasca  39232  dvavbase  39239  dvafvadd  39240  dvafvsca  39242  tendocnv  39247  dvhsca  39308  dvhfplusr  39310  dvhvbase  39313  dvhfvadd  39317  dvhfvsca  39326  lcdvadd  39823  lcdsbase  39826  lcdsadd  39827  lcdvs  39829  lcd0  39834  lcd1  39835  lcdneg  39836  mplascl0  40480  fsuppind  40489  imaiinfv  40725  mapfzcons1  40749  rexrabdioph  40826  dnnumch1  41080  dnwech  41084  aomclem6  41095  pwssplit4  41125  pwfi2f1o  41132  mendplusgfval  41221  mendvscafval  41226  harval3  41373  dssmapntrcls  41966  scotteqd  42083  colleq12d  42099  uzmptshftfval  42192  dropab1  42293  dropab2  42294  rabbida2  42910  rabbida3  42913  itgsinexplem1  43739  wallispi2lem2  43857  fourierdlem36  43928  etransclem4  44023  fcoreslem1  44816  afveq12d  44884  aoveq123d  44929  aovfundmoveq  44932  aovnuoveq  44942  aovvoveq  44943  aovovn0oveq  44945  afv2eq12d  44966  fsumsplitsndif  45084  rngccofvalALTV  45804  ringccofvalALTV  45867  rhmsubclem2  45904  rhmsubcALTVlem2  45922  itscnhlinecirc02plem2  46388  setrecseq  46650  aacllem  46764