Theorem 3eqtr4a 2797

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr4a.1	⊢ 𝐴 = 𝐵
3eqtr4a.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4a.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4a	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr4a

Step	Hyp	Ref	Expression
1		3eqtr4a.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3eqtr4a.1	. . 3 ⊢ 𝐴 = 𝐵
3	1, 2	eqtrdi 2787	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2774	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728

This theorem is referenced by:  rabsnif  4625  uniintsn  4884  iinvdif  4974  iununi  4993  dmxpid  5784  rnxpid  6016  csbrn  6046  dmsnsnsn  6063  opswap  6072  xpcoid  6133  unizlim  6308  fvco4i  6790  fndmdifcom  6841  fmptsng  6961  fmptsnd  6962  csbov  7234  ordunisuc  7589  offres  7734  1stval2  7756  2ndval2  7757  cnvf1olem  7856  fparlem3  7860  fparlem4  7861  frrlem12  8016  seqomlem1  8164  ecovcom  8483  ecovass  8484  ecovdi  8485  resixpfo  8595  mapunen  8793  cardidm  9540  cardiun  9563  alephcard  9649  cardalephex  9669  cardcf  9831  cfidm  9854  alephsing  9855  itunisuc  9998  itunitc  10000  ituniiun  10001  alephadd  10156  alephreg  10161  pwcfsdom  10162  addcompq  10529  addcomnq  10530  mulcompq  10531  mulcomnq  10532  addassnq  10537  mulassnq  10538  addid1  10977  zeo  12228  xnegneg  12769  xaddcom  12795  xaddid1  12796  xnegdi  12803  xmulid1  12834  xadddilem  12849  ixxin  12917  fzsuc2  13135  expneg  13608  sq01  13757  facp1  13809  bcpasc  13852  hashfzp1  13963  resunimafz0  13974  hashf1lem1  13985  hashf1lem1OLD  13986  hashf1  13988  ccat1st1st  14152  swrdccatin1  14255  swrdccat3blem  14269  repswsymballbi  14310  cshwmodn  14325  cshwlen  14329  repswcshw  14342  trclun  14542  relexpcnv  14563  relexpaddd  14582  absexp  14833  sqreulem  14888  fsumf1o  15252  fsumadd  15268  fsumrev2  15309  fsumparts  15333  fsumrelem  15334  fprodf1o  15471  fprodmul  15485  fproddiv  15486  fprodfac  15498  fallfacfwd  15561  efexp  15625  tanval2  15657  sadeq  15994  smumullem  16014  smumul  16015  gcdcom  16035  gcd0id  16041  gcdass  16070  lcmcom  16113  lcmneg  16123  lcmass  16134  nn0gcdsq  16271  dfphi2  16290  pcneg  16390  setscom  16709  strfvi  16718  setsnid  16720  ressbas  16738  ressinbas  16744  ressress  16746  firest  16891  topnval  16893  xpsfeq  17022  xpsaddlem  17032  xpsvsca  17036  oppchomfval  17171  oppchomfvalOLD  17172  oppcbas  17176  rescbas  17288  rescco  17291  resccoOLD  17292  cofuass  17349  fucbas  17422  fuchom  17423  fuchomOLD  17424  setccatid  17544  estrccatid  17593  xpcbas  17639  oduleval  17751  odulub  17867  oduglb  17869  ipotset  17993  efmndbas  18252  efmndbasabf  18253  symggrplem  18265  smndex1mndlem  18290  pwmnd  18318  grpinvfvi  18364  cntrval  18667  cntzval  18669  oppgplusfval  18694  snsymgefmndeq  18741  symgvalstruct  18743  pmtrprfval  18833  m1expaddsub  18844  sylow1lem2  18942  sylow3lem1  18970  oppglsm  18985  gsumzsplit  19266  gsum2dlem2  19310  gsumcom2  19314  dprd2dlem2  19381  dprd2da  19383  dmdprdsplit2lem  19386  mgpplusg  19462  mgpress  19469  ringidval  19472  opprmulfval  19597  abvtrivd  19830  sralem  20168  srasca  20172  sravsca  20173  sraip  20174  rlmval  20182  zlmlem  20437  zlmsca  20441  zlmvsca  20442  psgninv  20498  ocvval  20583  thlbas  20612  thlle  20613  thloc  20615  dsmmval2  20652  psrmulr  20863  mplmonmul  20947  mplcoe3  20949  opsrbaslem  20960  opsrtoslem2  20967  psr1val  21061  ply1basfvi  21116  ply1plusgfvi  21117  psr1sca2  21126  evl1fval1lem  21200  mattpos1  21307  mdettpos  21462  smadiadetglem1  21522  tgdif0  21843  indislem  21851  restco  22015  txtopon  22442  txindislem  22484  qtopres  22549  hmphindis  22648  ptuncnv  22658  snclseqg  22967  tsmssplit  23003  ussval  23111  tuslem  23118  setsmsbas  23327  tnglem  23492  tngds  23500  tngtset  23501  pcoass  23875  cphsqrtcl2  24037  rrxcph  24243  ovolunlem1a  24347  ioorinv  24427  itg11  24542  itg1mulc  24556  itg2cnlem1  24613  iblss2  24657  ibladdlem  24671  itgfsum  24678  iblabslem  24679  iblabs  24680  ditgneg  24708  deg1fvi  24937  dgrco  25123  logfac  25443  cxpexp  25510  cxpmul2  25531  cxpsqrt  25545  cxpsqrtth  25571  dvcxp1  25580  dvcxp2  25581  ang180lem1  25646  mcubic  25684  quart1  25693  reasinsin  25733  atanlogaddlem  25750  atantayl2  25775  log2tlbnd  25782  basellem2  25918  basellem3  25919  basellem5  25921  basellem8  25924  dchrmulid2  26087  bcp1ctr  26114  lgsneg  26156  lgsneg1  26157  lgsdir2  26165  lgsdir  26167  lgsdi  26169  lgsquad2lem2  26220  pntleml  26446  motgrp  26588  lmiisolem  26841  ttglem  26921  egrsubgr  27319  iswwlksnon  27891  iswspthsnon  27894  bafval  28639  ipidsq  28745  ipasslem1  28866  pjclem2  30231  cvmdi  30359  imadifxp  30613  2ndimaxp  30657  iundisjcnt  30793  dpfrac1  30840  gsumpart  30988  cycpmco2rn  31065  cyc3genpmlem  31091  resvsca  31202  rspectset  31484  indval2  31648  bayesth  32072  ofcccat  32188  plymulx  32193  subfacp1lem6  32814  satfdm  32998  mvtval  33129  mexval  33131  mexval2  33132  mdvval  33133  mrsubfval  33137  mrsubvrs  33151  msubfval  33153  elmsubrn  33157  mvhfval  33162  mpstval  33164  msrfval  33166  mstaval  33173  mthmval  33204  bccolsum  33374  dfrdg2  33441  dfrdg3  33442  lrold  33763  dfrdg4  33939  ordtoplem  34310  ordcmp  34322  curunc  35445  matunitlindflem2  35460  poimirlem6  35469  poimirlem7  35470  poimirlem11  35474  poimirlem12  35475  poimirlem13  35476  poimirlem14  35477  poimirlem16  35479  poimirlem19  35482  poimirlem21  35484  poimirlem22  35485  poimirlem27  35490  poimirlem31  35494  poimirlem32  35495  itg2addnclem2  35515  ibladdnclem  35519  iblabsnclem  35526  iblabsnc  35527  iblmulc2nc  35528  ftc1anclem8  35543  pmodN  37550  tgrpgrplem  38449  tendoplass  38483  tendoicl  38496  erngdvlem3  38690  dvhvaddass  38797  dib0  38864  dib1dim2  38868  diclspsn  38894  cdlemn8  38904  dihopelvalcpre  38948  djhcom  39105  nn0expgcd  39984  kelac2  40534  mendbas  40653  mendsca  40658  mendring  40661  iscard4  40766  relexp01min  40939  relexpaddss  40944  iotain  41649  addrcom  41707  rnsnf  42335  itgsinexplem1  43113  volioc  43131  dirkertrigeqlem1  43257  fourierdlem104  43369  sqwvfoura  43387  sqwvfourb  43388  fzopredsuc  44431  fppr2odd  44799  rngccatidALTV  45163  ringccatidALTV  45226  0dig2pr01  45572  nn0sumshdiglemB  45582