Theorem 3eqtr4g 2838

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

Syntax hints:   → wi 4   = wceq 1601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2769

This theorem is referenced by:  rabbidva2  3382  rabeqf  3386  csbeq1  3753  csbeq2  3754  difeq1  3943  difeq2  3944  uneq2  3983  ineq2  4030  symdifeq1  4068  symdifeq2  4069  dfrab3ss  4130  csbprc  4205  csbeq2d  4215  csbnestgf  4220  disjssun  4259  ifeq1  4310  ifeq2  4311  pweq  4381  sneq  4407  csbsng  4474  csbprg  4475  preq1  4499  preq2  4500  tpeq1  4508  tpeq2  4509  tpeq3  4510  prprc1  4531  tpprceq3  4566  opeq1  4636  opeq2  4637  oteq1  4645  oteq2  4646  oteq3  4647  csbopg  4654  unieq  4679  csbuni  4701  inteq  4713  iineq1  4768  iineq2  4771  dfiin2g  4786  iinrab  4815  iinin1  4824  iinxprg  4834  iununi  4844  opabbid  4951  mpteq12f  4967  mpteq12df  4970  csbmpt12  5247  xpeq1  5369  xpeq2  5376  rneq  5596  reseq1  5636  reseq2  5637  resima2  5681  resindm  5694  resmpt  5699  resmptf  5701  imaeq1  5715  imaeq2  5716  mptcnv  5789  xpdisj1  5809  xpdisj2  5810  resdisj  5817  dmpropg  5862  rnpropg  5869  cores  5892  cores2  5902  xpco  5929  predeq123  5934  sspred  5941  suceq  6041  sucprc  6051  iotaeq  6107  iotabi  6108  fntpg  6194  imain  6219  f1oprswap  6434  fveq1  6445  fveq2  6446  fvres  6465  csbfv12  6490  fnimapr  6522  fvco2  6533  residpr  6674  fsnunfv  6724  fsnunres  6725  funiunfv  6778  fliftf  6837  isoini2  6861  riotaeqdv  6884  riotabidv  6885  riotauni  6889  riotabidva  6899  snriota  6913  oveq  6928  oveq1  6929  oveq2  6930  oprabbid  6985  mpt2eq123  6991  mpt2eq123dva  6993  mpt2eq3dva  6996  resmpt2  7035  ovres  7077  f1ocnvd  7161  ofeq  7176  ofreq  7177  fpar  7562  wrecseq123  7690  onovuni  7722  recseq  7753  tfr2a  7774  rdgeq1  7790  rdgeq2  7791  rdgsucmptf  7807  frsucmpt  7816  seqomeq12  7832  seqomsuc  7835  omopthi  8021  eceq1  8064  eceq2  8066  qseq1  8078  qseq2  8079  uniqs  8090  ecinxp  8105  qsinxp  8106  erovlem  8127  ecopovtrn  8134  ixpeq1  8205  supeq1  8639  supeq2  8642  supeq3  8643  supeq123d  8644  infeq1  8670  infeq2  8673  infeq3  8674  infeq123d  8675  infiso  8702  oieq1  8706  oieq2  8707  ordtypelem1  8712  inf3lemc  8820  wemapwe  8891  r1sucg  8929  r1limg  8931  rankprb  9011  karden  9055  djueq12  9064  cardiun  9141  acneq  9199  alephlim  9223  alephsuc  9224  alephfplem2  9261  infpssrlem2  9461  fin23lem34  9503  fin23lem35  9504  zorn2lem1  9653  zorn2lem7  9659  fpwwe2lem6  9792  fpwwe2lem13  9799  addpiord  10041  mulpiord  10042  addpqnq  10095  mulpqnq  10098  addassnq  10115  mulassnq  10116  distrnq  10118  lterpq  10127  ltexnq  10132  ltsrpr  10234  00sr  10256  recexsrlem  10260  mulgt0sr  10262  addcnsrec  10300  mulcnsrec  10301  negeq  10614  csbnegg  10619  negsubdi  10679  mulneg1  10811  negfi  11325  deceq1  11850  deceq2  11851  xnegeq  12350  fseq1p1m1  12732  om2uzrdg  13074  uzrdgsuci  13078  seqeq1  13122  seqeq2  13123  seqeq3  13124  seqfeq4  13168  seqof  13176  hashprg  13497  hashtpg  13581  csbwrdg  13633  s1eq  13690  cats1co  14007  s2eqd  14014  s3eqd  14015  s4eqd  14016  s5eqd  14017  s6eqd  14018  s7eqd  14019  s8eqd  14020  xpcogend  14122  shftval  14221  limsupgle  14616  lo1eq  14707  rlimeq  14708  sumeq1  14827  sumeq2w  14830  sumeq2ii  14831  zsum  14856  sumss2  14864  fsumsplitsnun  14891  isumclim3  14895  fsumcom2  14910  incexclem  14972  incexc2  14974  isumshft  14975  prodeq1f  15041  prodeq2w  15045  prodeq2ii  15046  zprod  15070  fprodm1s  15103  fprodp1s  15104  fprodcom2  15117  fprodsplitf  15121  iprodclim3  15133  ef0lem  15211  ruclem7  15369  sadcp1  15583  smupp1  15608  smueqlem  15618  algrp1  15693  dfphi2  15883  prmdiveq  15895  pceulem  15954  vdwlem6  16094  cshwsiun  16205  sloteq  16260  setsid  16310  elbasfv  16316  elbasov  16317  imastset  16568  imasvscaval  16584  xpscg  16604  isoval  16810  funcoppc  16920  fulloppc  16967  fuccofval  17004  natpropd  17021  catccofval  17135  xpchomfval  17205  xpccofval  17208  lubfval  17364  glbfval  17377  grpidpropd  17647  gsumpropd2lem  17659  frmdplusg  17778  grpinvpropd  17877  grpsubpropd  17907  grpsubpropd2  17908  mulgpropd  17968  oppgmnd  18167  symgplusg  18192  sylow1lem2  18398  sylow3lem1  18426  prds1  19001  pwsmgp  19005  opprring  19018  rngidpropd  19082  dvdsrpropd  19083  unitpropd  19084  invrpropd  19085  rhm1  19119  lmhmpropd  19468  lidlrsppropd  19627  lpival  19642  ressascl  19741  asclpropd  19743  aspval2  19744  psrbas  19775  psrplusg  19778  psrmulr  19781  psrvscafval  19787  resspsrbas  19812  ressmplbas2  19852  opsrle  19872  opsrbaslem  19874  vr1val  19958  ressply1add  19996  ressply1mul  19997  ressply1vsca  19998  psrplusgpropd  20002  mplbaspropd  20003  psropprmul  20004  ply1baspropd  20009  ply1plusgpropd  20010  ply1sca2  20020  subrgvr1  20027  coe1mul2lem2  20034  ply1coe1eq  20064  zrhpropd  20259  znle  20280  frlmplusgval  20507  frlmvscafval  20509  mamudi  20613  mamudir  20614  matrcl  20622  oftpos  20663  mattpos1  20667  mdetfval  20797  mdetrlin  20813  mdetrsca  20814  mdetrsca2  20815  mdetrlin2  20818  mdetunilem5  20827  madufval  20848  madugsum  20854  idmatidpmat  20949  cpmidpmat  21085  cncmp  21604  2ndcsep  21671  llyeq  21682  nllyeq  21683  xkouni  21811  hmphindis  22009  xkocnv  22026  ptcmplem2  22265  snclseqg  22327  prdstmdd  22335  ustexsym  22427  ucnextcn  22516  metreslem  22575  comet  22726  nrmmetd  22787  nmpropd  22806  isngp3  22810  ngpds  22816  subgnm  22845  tngnm  22863  idnghm  22955  cnmetdval  22982  cnmpt2pc  23135  htpyco2  23186  phtpyco2  23197  clsocv  23456  rrxprds  23595  rrxnm  23597  rrxplusgvscavalb  23601  ovolunlem1a  23700  voliunlem3  23756  ioombl1lem4  23765  uniioombllem4  23790  itg11  23895  itgeq1f  23975  itgeq2  23981  iblss2  24009  itgss  24015  itgeqa  24017  itgfsum  24030  itgsplit  24039  ditgeq1  24049  ditgeq2  24050  ditgeq3  24051  dvcmulf  24145  dvmptfsum  24175  dvcnvrelem2  24218  mdegfval  24259  mdegpropd  24281  deg1propd  24283  plyeq0  24404  coe11  24446  dgrlt  24459  dgradd2  24461  dgrmulc  24464  dvply1  24476  fta1lem  24499  pserulm  24613  rlimcnp2  25145  jensenlem1  25165  basellem5  25263  dchrbas  25412  dchrrcl  25417  dchrplusg  25424  dchrfi  25432  lgsdi  25511  lgseisenlem2  25553  lgsquadlem3  25559  dchrmusumlema  25634  rpvmasum2  25653  dchrisum0lema  25655  pntlemg  25739  colperpexlem2  26079  axlowdimlem13  26303  uhgrvtxedgiedgb  26484  uhgrvtxedgiedgbOLD  26485  nb3grprlem1  26728  crctcshlem2  27167  wpthswwlks2on  27341  clwlknf1oclwwlkn  27483  clwlknf1oclwwlknOLD  27485  frgrncvvdeq  27717  avril1  27894  0vfval  28033  imsval  28112  imsdval  28113  bcseqi  28549  normpythi  28571  cm0  29040  fh1  29049  pjcji  29115  opsqrlem5  29575  pjsdi2i  29588  pjclem3  29628  pjci  29631  golem1  29702  iunrdx  29944  ofresid  30009  f1od2  30065  dp2eq1  30143  dp2eq2  30144  gsumvsca1  30344  gsumvsca2  30345  rhmopp  30381  resv1r  30399  lindsunlem  30438  fzto1st1  30450  crefeq  30510  xrge0mulc1cn  30585  qqhval2  30624  esumeq12dvaf  30691  esumeq2  30696  esumf1o  30710  esumfzf  30729  esumss  30732  esumpfinvalf  30736  ofceq  30757  carsgclctunlem1  30977  itgeq12dv  30986  ccatmulgnn0dir  31219  breprexpnat  31314  bnj956  31446  bnj1385  31502  bnj96  31534  bnj548  31566  bnj553  31567  bnj554  31568  bnj602  31584  bnj18eq1  31596  bnj1234  31680  bnj1296  31688  bnj1318  31692  bnj1442  31716  bnj1450  31717  cvmliftlem5  31870  cvmliftlem10  31875  cvmlift2lem9  31892  cvmliftphtlem  31898  mthmpps  32078  eqfunressuc  32253  rdgprc  32288  dfrdg2  32289  trpredeq1  32308  trpredeq2  32309  trpredeq3  32310  wsuceq123  32348  wlimeq12  32353  frecseq123  32366  nosupbnd2lem1  32450  altopthsn  32657  altxpeq1  32669  altxpeq2  32670  ee7.2aOLD  33043  bj-rabbida2  33486  bj-sngleq  33527  bj-tageq  33536  bj-projeq  33552  bj-projval  33556  bj-1upleq  33559  bj-pr1eq  33562  bj-pr2eq  33576  bj-evaleq  33597  bj-imafv  33728  csbpredg  33768  csbwrecsg  33769  csbrecsg  33770  csbrdgg  33771  csboprabg  33772  csbmpt22g  33773  finxpeq1  33818  finxpeq2  33819  csbfinxpg  33820  finxpreclem4  33826  cureq  33994  unceq  33995  uncov  33999  unccur  34001  finixpnum  34003  ptrest  34018  poimirlem3  34022  poimirlem9  34028  poimirlem15  34034  poimirlem16  34035  poimirlem26  34045  poimirlem27  34046  mbfposadd  34066  cnambfre  34067  iblabsnclem  34082  ftc1anclem1  34094  heiborlem4  34221  heiborlem6  34223  mpt2bi123f  34577  iineq12f  34579  mptbi12f  34581  eccnvepres  34661  uniqsALTV  34713  xrneq1  34751  xrneq2  34754  cosseq  34793  redss3  34981  riotaclbgBAD  35092  toycom  35111  ldualvbase  35264  ldualfvadd  35266  ldualsca  35270  ldualsbase  35271  ldualsaddN  35272  ldualfvs  35274  ldual0  35285  ldual1  35286  ldualneg  35287  cdleme19f  36446  cdleme20m  36461  cdleme21k  36476  cdleme27b  36506  cdleme31so  36517  cdleme31sn  36518  cdleme31se  36520  cdleme31se2  36521  cdleme31sc  36522  cdleme31sde  36523  cdleme31fv  36528  cdleme40v  36607  cdleme43dN  36630  cdlemeg46ngfr  36656  ltrnco4  36877  tgrpbase  36884  tgrpopr  36885  erngbase  36939  erngfplus  36940  erngfmul  36943  erngbase-rN  36947  erngfplus-rN  36948  erngfmul-rN  36951  dvasca  37144  dvavbase  37151  dvafvadd  37152  dvafvsca  37154  tendocnv  37159  dvhsca  37220  dvhfplusr  37222  dvhvbase  37225  dvhfvadd  37229  dvhfvsca  37238  lcdvadd  37735  lcdsbase  37738  lcdsadd  37739  lcdvs  37741  lcd0  37746  lcd1  37747  lcdneg  37748  imaiinfv  38198  mapfzcons1  38222  rexrabdioph  38300  dnnumch1  38555  dnwech  38559  aomclem6  38570  pwssplit4  38600  pwfi2f1o  38607  mendplusgfval  38696  mendvscafval  38701  dssmapntrcls  39364  uzmptshftfval  39483  dropab1  39587  dropab2  39588  rabbida2  40226  rabbida3  40229  itgsinexplem1  41079  wallispi2lem2  41198  fourierdlem36  41269  etransclem4  41364  afveq12d  42156  aoveq123d  42201  aovfundmoveq  42204  aovnuoveq  42214  aovvoveq  42215  aovovn0oveq  42217  afv2eq12d  42238  fsumsplitsndif  42357  rngccofvalALTV  42984  ringccofvalALTV  43047  rhmsubclem2  43084  rhmsubcALTVlem2  43102  xpprsng  43107  itscnhlinecirc02plem2  43501  setrecseq  43519  aacllem  43635