Theorem 3eqtr4g 2681

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

Syntax hints:   → wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  rabbidva2  3186  rabeqf  3190  csbeq1  3536  csbeq2  3537  difeq1  3721  difeq2  3722  uneq2  3761  ineq2  3808  symdifeq1  3846  symdifeq2  3847  dfrab3ss  3905  csbprc  3980  csbeq2d  3991  csbnestgf  3996  disjssun  4036  ifeq1  4090  ifeq2  4091  pweq  4161  sneq  4187  csbsng  4243  csbprg  4244  rabsn  4256  preq1  4268  preq2  4269  tpeq1  4277  tpeq2  4278  tpeq3  4279  prprc1  4300  tpprceq3  4335  opeq1  4402  opeq2  4403  oteq1  4411  oteq2  4412  oteq3  4413  csbopg  4420  unieq  4444  csbuni  4466  inteq  4478  iineq1  4535  iineq2  4538  dfiin2g  4553  iinrab  4582  iinin1  4591  iinxprg  4601  iununi  4610  opabbid  4715  mpteq12f  4731  mpteq12d  4734  mpteq12df  4735  csbmpt12  5010  xpeq1  5128  xpeq2  5129  rneq  5351  reseq1  5390  reseq2  5391  resima2  5432  resindm  5444  resmpt  5449  resmptf  5451  imaeq1  5461  imaeq2  5462  mptcnv  5534  xpdisj1  5555  xpdisj2  5556  resdisj  5563  dmpropg  5608  rnpropg  5615  cores  5638  cores2  5648  xpco  5675  predeq123  5681  sspred  5688  suceq  5790  sucprc  5800  iotaeq  5859  iotabi  5860  fntpg  5948  imain  5974  f1oprswap  6180  fveq1  6190  fveq2  6191  fvres  6207  csbfv12  6231  fnimapr  6262  fvco2  6273  residpr  6409  fsnunfv  6453  fsnunres  6454  funiunfv  6506  fliftf  6565  isoini2  6589  riotaeqdv  6612  riotabidv  6613  riotauni  6617  riotabidva  6627  snriota  6641  oveq  6656  oveq1  6657  oveq2  6658  oprabbid  6708  mpt2eq123  6714  mpt2eq123dva  6716  mpt2eq3dva  6719  resmpt2  6758  ovres  6800  f1ocnvd  6884  ofeq  6899  ofreq  6900  fpar  7281  wrecseq123  7408  onovuni  7439  recseq  7470  tfr2a  7491  rdgeq1  7507  rdgeq2  7508  rdgsucmptf  7524  frsucmpt  7533  seqomeq12  7549  seqomsuc  7552  omopthi  7737  eceq1  7782  eceq2  7784  qseq1  7796  qseq2  7797  uniqs  7807  ecinxp  7822  qsinxp  7823  erovlem  7843  ecopovtrn  7850  ixpeq1  7919  supeq1  8351  supeq2  8354  supeq3  8355  supeq123d  8356  infeq1  8382  infeq2  8385  infeq3  8386  infeq123d  8387  infiso  8413  oieq1  8417  oieq2  8418  ordtypelem1  8423  inf3lemc  8523  wemapwe  8594  r1sucg  8632  r1limg  8634  rankprb  8714  karden  8758  cardiun  8808  acneq  8866  alephlim  8890  alephsuc  8891  alephfplem2  8928  infpssrlem2  9126  fin23lem34  9168  fin23lem35  9169  zorn2lem1  9318  zorn2lem7  9324  fpwwe2lem6  9457  fpwwe2lem13  9464  addpiord  9706  mulpiord  9707  addpqnq  9760  mulpqnq  9763  addassnq  9780  mulassnq  9781  distrnq  9783  lterpq  9792  ltexnq  9797  ltsrpr  9898  00sr  9920  recexsrlem  9924  mulgt0sr  9926  addcnsrec  9964  mulcnsrec  9965  negeq  10273  csbnegg  10278  negsubdi  10337  mulneg1  10466  negfi  10971  deceq1  11500  deceq1OLD  11501  deceq2  11502  deceq2OLD  11503  xnegeq  12038  fseq1p1m1  12414  om2uzrdg  12755  uzrdgsuci  12759  seqeq1  12804  seqeq2  12805  seqeq3  12806  seqfeq4  12850  seqof  12858  hashprg  13182  hashprgOLD  13183  hashmap  13222  hashtpg  13267  csbwrdg  13334  s1eq  13380  cats1co  13601  s2eqd  13608  s3eqd  13609  s4eqd  13610  s5eqd  13611  s6eqd  13612  s7eqd  13613  s8eqd  13614  xpcogend  13713  shftval  13814  limsupgle  14208  lo1eq  14299  rlimeq  14300  sumeq1  14419  sumeq2w  14422  sumeq2ii  14423  zsum  14449  sumss2  14457  fsumsplitsnun  14484  fsumsplitsnunOLD  14486  isumclim3  14490  fsumcom2  14505  fsumcom2OLD  14506  incexclem  14568  incexc2  14570  isumshft  14571  prodeq1f  14638  prodeq2w  14642  prodeq2ii  14643  zprod  14667  fprodm1s  14700  fprodp1s  14701  fprodcom2  14714  fprodcom2OLD  14715  iprodclim3  14731  ef0lem  14809  ruclem7  14965  sadcp1  15177  smupp1  15202  smueqlem  15212  algrp1  15287  dfphi2  15479  prmdiveq  15491  pceulem  15550  vdwlem6  15690  cshwsiun  15806  sloteq  15862  setsid  15914  elbasfv  15920  elbasov  15921  imastset  16182  imasvscaval  16198  xpscg  16218  isoval  16425  funcoppc  16535  fulloppc  16582  fuccofval  16619  natpropd  16636  catccofval  16750  xpchomfval  16819  xpccofval  16822  lubfval  16978  glbfval  16991  grpidpropd  17261  gsumpropd2lem  17273  frmdplusg  17391  grpinvpropd  17490  grpsubpropd  17520  grpsubpropd2  17521  mulgpropd  17584  oppgmnd  17784  symgplusg  17809  sylow1lem2  18014  sylow3lem1  18042  prds1  18614  pwsmgp  18618  opprring  18631  rngidpropd  18695  dvdsrpropd  18696  unitpropd  18697  invrpropd  18698  rhm1  18730  lmhmpropd  19073  lidlrsppropd  19230  lpival  19245  ressascl  19344  asclpropd  19346  aspval2  19347  psrbas  19378  psrplusg  19381  psrmulr  19384  psrvscafval  19390  resspsrbas  19415  ressmplbas2  19455  opsrle  19475  opsrbaslem  19477  opsrbaslemOLD  19478  vr1val  19562  ressply1add  19600  ressply1mul  19601  ressply1vsca  19602  psrplusgpropd  19606  mplbaspropd  19607  psropprmul  19608  ply1baspropd  19613  ply1plusgpropd  19614  ply1sca2  19624  subrgvr1  19631  coe1mul2lem2  19638  ply1coe1eq  19668  zrhpropd  19863  znle  19884  frlmplusgval  20107  frlmvscafval  20109  mamudi  20209  mamudir  20210  matrcl  20218  oftpos  20258  mattpos1  20262  mdetfval  20392  mdetrlin  20408  mdetrsca  20409  mdetrsca2  20410  mdetrlin2  20413  mdetunilem5  20422  madufval  20443  madugsum  20449  idmatidpmat  20542  cpmidpmat  20678  cncmp  21195  2ndcsep  21262  llyeq  21273  nllyeq  21274  xkouni  21402  hmphindis  21600  xkocnv  21617  ptcmplem2  21857  snclseqg  21919  prdstmdd  21927  ustexsym  22019  ucnextcn  22108  metreslem  22167  comet  22318  nrmmetd  22379  nmpropd  22398  isngp3  22402  ngpds  22408  subgnm  22437  tngnm  22455  idnghm  22547  cnmetdval  22574  cnmpt2pc  22727  htpyco2  22778  phtpyco2  22789  clsocv  23049  rrxprds  23177  rrxnm  23179  ovolunlem1a  23264  voliunlem3  23320  ioombl1lem4  23329  uniioombllem4  23354  itg11  23458  itgeq1f  23538  itgeq2  23544  iblss2  23572  itgss  23578  itgeqa  23580  itgfsum  23593  itgsplit  23602  ditgeq1  23612  ditgeq2  23613  ditgeq3  23614  dvcmulf  23708  dvmptfsum  23738  dvcnvrelem2  23781  mdegfval  23822  mdegpropd  23844  deg1propd  23846  plyeq0  23967  coe11  24009  dgrlt  24022  dgradd2  24024  dgrmulc  24027  dvply1  24039  fta1lem  24062  pserulm  24176  rlimcnp2  24693  jensenlem1  24713  basellem5  24811  dchrbas  24960  dchrrcl  24965  dchrplusg  24972  dchrfi  24980  lgsdi  25059  lgseisenlem2  25101  lgsquadlem3  25107  dchrmusumlema  25182  rpvmasum2  25201  dchrisum0lema  25203  pntlemg  25287  colperpexlem2  25623  axlowdimlem13  25834  uhgrvtxedgiedgb  26031  nb3grprlem1  26282  crctcshlem2  26710  frgrncvvdeq  27173  avril1  27319  0vfval  27461  imsval  27540  imsdval  27541  bcseqi  27977  normpythi  27999  cm0  28468  fh1  28477  pjcji  28543  opsqrlem5  29003  pjsdi2i  29016  pjclem3  29056  pjci  29059  golem1  29130  iunrdx  29382  ofresid  29444  f1od2  29499  dp2eq1  29580  dp2eq2  29581  gsumvsca1  29782  gsumvsca2  29783  rhmopp  29819  resv1r  29837  fzto1st1  29852  crefeq  29912  xrge0mulc1cn  29987  qqhval2  30026  esumeq12dvaf  30093  esumeq2  30098  esumf1o  30112  esumfzf  30131  esumss  30134  esumpfinvalf  30138  ofceq  30159  carsgclctunlem1  30379  itgeq12dv  30388  ccatmulgnn0dir  30619  breprexpnat  30712  bnj956  30847  bnj1385  30903  bnj96  30935  bnj548  30967  bnj553  30968  bnj554  30969  bnj602  30985  bnj18eq1  30997  bnj1234  31081  bnj1296  31089  bnj1318  31093  bnj1442  31117  bnj1450  31118  cvmliftlem5  31271  cvmliftlem10  31276  cvmlift2lem9  31293  cvmliftphtlem  31299  mthmpps  31479  eqfunressuc  31660  rdgprc  31700  dfrdg2  31701  trpredeq1  31720  trpredeq2  31721  trpredeq3  31722  wsuceq123  31760  wlimeq12  31765  nosupbnd2lem1  31861  altopthsn  32068  altxpeq1  32080  altxpeq2  32081  ee7.2aOLD  32460  bj-rabbida2  32913  bj-sngleq  32955  bj-tageq  32964  bj-projeq  32980  bj-projval  32984  bj-1upleq  32987  bj-pr1eq  32990  bj-pr2eq  33004  bj-evaleq  33024  csbpredg  33172  csbwrecsg  33173  csbrecsg  33174  csbrdgg  33175  csboprabg  33176  csbmpt22g  33177  finxpeq1  33223  finxpeq2  33224  csbfinxpg  33225  finxpreclem4  33231  cureq  33385  unceq  33386  uncov  33390  unccur  33392  finixpnum  33394  ptrest  33408  poimirlem3  33412  poimirlem9  33418  poimirlem15  33424  poimirlem16  33425  poimirlem26  33435  poimirlem27  33436  mbfposadd  33457  cnambfre  33458  iblabsnclem  33473  ftc1anclem1  33485  heiborlem4  33613  heiborlem6  33615  mpt2bi123f  33971  iineq12f  33973  mptbi12f  33975  eccnvepres  34045  uniqsALTV  34101  riotaclbgBAD  34240  toycom  34260  ldualvbase  34413  ldualfvadd  34415  ldualsca  34419  ldualsbase  34420  ldualsaddN  34421  ldualfvs  34423  ldual0  34434  ldual1  34435  ldualneg  34436  cdleme19f  35596  cdleme20m  35611  cdleme21k  35626  cdleme27b  35656  cdleme31so  35667  cdleme31sn  35668  cdleme31se  35670  cdleme31se2  35671  cdleme31sc  35672  cdleme31sde  35673  cdleme31fv  35678  cdleme40v  35757  cdleme43dN  35780  cdlemeg46ngfr  35806  ltrnco4  36027  tgrpbase  36034  tgrpopr  36035  erngbase  36089  erngfplus  36090  erngfmul  36093  erngbase-rN  36097  erngfplus-rN  36098  erngfmul-rN  36101  dvasca  36294  dvavbase  36301  dvafvadd  36302  dvafvsca  36304  tendocnv  36310  dvhsca  36371  dvhfplusr  36373  dvhvbase  36376  dvhfvadd  36380  dvhfvsca  36389  lcdvadd  36886  lcdsbase  36889  lcdsadd  36890  lcdvs  36892  lcd0  36897  lcd1  36898  lcdneg  36899  imaiinfv  37256  mapfzcons1  37280  rexrabdioph  37358  dnnumch1  37614  dnwech  37618  aomclem6  37629  pwssplit4  37659  pwfi2f1o  37666  mendplusgfval  37755  mendvscafval  37760  dssmapntrcls  38426  uzmptshftfval  38545  dropab1  38651  dropab2  38652  csbunigOLD  39051  csbfv12gALTOLD  39052  csbxpgOLD  39053  csbresgOLD  39055  csbrngOLD  39056  csbima12gALTOLD  39057  rabbida2  39317  rabbida3  39320  itgsinexplem1  40169  wallispi2lem2  40289  fourierdlem36  40360  etransclem4  40455  afveq12d  41213  aoveq123d  41258  aovfundmoveq  41261  aovnuoveq  41271  aovvoveq  41272  aovovn0oveq  41274  fsumsplitsndif  41343  rngccofvalALTV  41987  ringccofvalALTV  42050  rhmsubclem2  42087  rhmsubcALTVlem2  42105  xpprsng  42110  setrecseq  42432  aacllem  42547