Theorem 3eqtr4a 2796

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 2786	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2773	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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  rabsnif  4699  uniintsn  4961  iinvdif  5056  iununi  5075  dmxpid  5910  rnxpid  6162  csbrn  6192  dmsnsnsn  6209  opswap  6218  xpcoid  6279  predres  6328  unizlim  6476  fvco4i  6979  fndmdifcom  7032  fmptsng  7159  fmptsnd  7160  csbov  7448  ordunisuc  7824  offres  7980  1stval2  8003  2ndval2  8004  cnvf1olem  8107  fparlem3  8111  fparlem4  8112  frrlem12  8294  seqomlem1  8462  ecovcom  8835  ecovass  8836  ecovdi  8837  resixpfo  8948  mapunen  9158  cardidm  9971  cardiun  9994  alephcard  10082  cardalephex  10102  cardcf  10264  cfidm  10287  alephsing  10288  itunisuc  10431  itunitc  10433  ituniiun  10434  alephadd  10589  alephreg  10594  pwcfsdom  10595  addcompq  10962  addcomnq  10963  mulcompq  10964  mulcomnq  10965  addassnq  10970  mulassnq  10971  addrid  11413  zeo  12677  xnegneg  13228  xaddcom  13254  xaddrid  13255  xnegdi  13262  xmulrid  13293  xadddilem  13308  ixxin  13377  fzsuc2  13597  expneg  14085  sq01  14241  facp1  14294  bcpasc  14337  hashfzp1  14447  resunimafz0  14461  hashf1lem1  14471  hashf1  14473  ccat1st1st  14644  swrdccatin1  14741  swrdccat3blem  14755  repswsymballbi  14796  cshwmodn  14811  cshwlen  14815  repswcshw  14828  trclun  15031  relexpcnv  15052  relexpaddd  15071  absexp  15321  sqreulem  15376  fsumf1o  15737  fsumadd  15754  fsumrev2  15796  fsumparts  15820  fsumrelem  15821  fprodf1o  15960  fprodmul  15974  fproddiv  15975  fprodfac  15987  fallfacfwd  16050  efexp  16117  tanval2  16149  sadeq  16489  smumullem  16509  smumul  16510  gcdcom  16530  gcd0id  16536  gcdass  16564  nn0expgcd  16581  lcmcom  16610  lcmneg  16620  lcmass  16631  nn0gcdsq  16769  dfphi2  16791  pcneg  16892  setscom  17197  strfvi  17207  fveqprc  17208  oveqprc  17209  ressbas  17255  ressinbas  17264  ressress  17266  firest  17444  topnval  17446  xpsfeq  17575  xpsaddlem  17585  xpsvsca  17589  oppchomfval  17724  rescbas  17840  rescco  17843  cofuass  17900  fucbas  17974  fuchom  17975  setccatid  18095  estrccatid  18142  xpcbas  18188  oduleval  18299  odulub  18415  oduglb  18417  ipotset  18541  efmndbas  18847  efmndbasabf  18848  symggrplem  18860  smndex1mndlem  18885  pwmnd  18913  grpinvfvi  18963  cntrval  19300  cntzval  19302  oppgplusfval  19329  snsymgefmndeq  19374  symgvalstruct  19376  pmtrprfval  19466  m1expaddsub  19477  sylow1lem2  19578  sylow3lem1  19606  oppglsm  19621  gsumzsplit  19906  gsum2dlem2  19950  gsumcom2  19954  dprd2dlem2  20021  dprd2da  20023  dmdprdsplit2lem  20026  mgpplusg  20102  mgpress  20108  ringidval  20141  opprmulfval  20297  abvtrivd  20790  sralem  21132  srasca  21136  sravsca  21137  sraip  21138  rlmval  21147  zlmsca  21479  zlmvsca  21480  psgninv  21540  ocvval  21625  thlbas  21654  thlle  21655  thloc  21657  dsmmval2  21694  psrmulr  21900  mplmonmul  21992  mplcoe3  21994  opsrbaslem  22005  opsrtoslem2  22012  psr1val  22119  ply1basfvi  22174  ply1plusgfvi  22175  psr1sca2  22184  evl1fval1lem  22266  mattpos1  22392  mdettpos  22547  smadiadetglem1  22607  tgdif0  22928  indislem  22936  restco  23100  txtopon  23527  txindislem  23569  qtopres  23634  hmphindis  23733  ptuncnv  23743  snclseqg  24052  tsmssplit  24088  ussval  24196  tuslem  24203  setsmsbas  24412  tngds  24585  tngtset  24586  pcoass  24973  cphsqrtcl2  25136  rrxcph  25342  ovolunlem1a  25447  ioorinv  25527  itg11  25642  itg1mulc  25655  itg2cnlem1  25712  iblss2  25757  ibladdlem  25771  itgfsum  25778  iblabslem  25779  iblabs  25780  ditgneg  25808  deg1fvi  26040  dgrco  26231  logfac  26560  cxpexp  26627  cxpmul2  26648  cxpsqrt  26662  cxpsqrtth  26689  dvcxp1  26699  dvcxp2  26700  ang180lem1  26769  mcubic  26807  quart1  26816  reasinsin  26856  atanlogaddlem  26873  atantayl2  26898  log2tlbnd  26905  basellem2  27042  basellem3  27043  basellem5  27045  basellem8  27048  fsumdvdsmul  27155  dchrmullid  27213  bcp1ctr  27240  lgsneg  27282  lgsneg1  27283  lgsdir2  27291  lgsdir  27293  lgsdi  27295  lgsquad2lem2  27346  pntleml  27572  lrold  27852  abssnid  28184  om2noseqfo  28221  n0seo  28322  zs12bday  28341  motgrp  28468  lmiisolem  28721  egrsubgr  29202  iswwlksnon  29781  iswspthsnon  29784  bafval  30531  ipidsq  30637  ipasslem1  30758  pjclem2  32123  cvmdi  32251  imadifxp  32528  2ndimaxp  32570  suppun2  32607  iundisjcnt  32721  indval2  32777  dpfrac1  32812  gsumpart  32997  cycpmco2rn  33082  cyc3genpmlem  33108  fracbas  33245  resvsca  33294  rspectset  33843  bayesth  34417  ofcccat  34521  plymulx  34526  subfacp1lem6  35153  satfdm  35337  mvtval  35468  mexval  35470  mexval2  35471  mdvval  35472  mrsubfval  35476  mrsubvrs  35490  msubfval  35492  elmsubrn  35496  mvhfval  35501  mpstval  35503  msrfval  35505  mstaval  35512  mthmval  35543  bccolsum  35702  dfrdg2  35759  dfrdg3  35760  dfrdg4  35915  ordtoplem  36399  ordcmp  36411  curunc  37572  matunitlindflem2  37587  poimirlem6  37596  poimirlem7  37597  poimirlem11  37601  poimirlem12  37602  poimirlem13  37603  poimirlem14  37604  poimirlem16  37606  poimirlem19  37609  poimirlem21  37611  poimirlem22  37612  poimirlem27  37617  poimirlem31  37621  poimirlem32  37622  itg2addnclem2  37642  ibladdnclem  37646  iblabsnclem  37653  iblabsnc  37654  iblmulc2nc  37655  ftc1anclem8  37670  pmodN  39815  tgrpgrplem  40714  tendoplass  40748  tendoicl  40761  erngdvlem3  40955  dvhvaddass  41062  dib0  41129  dib1dim2  41133  diclspsn  41159  cdlemn8  41169  dihopelvalcpre  41213  djhcom  41370  evlsbagval  42536  kelac2  43036  mendbas  43151  mendring  43159  iscard4  43504  relexp01min  43684  relexpaddss  43689  iotain  44389  addrcom  44447  rnsnf  45156  itgsinexplem1  45931  volioc  45949  dirkertrigeqlem1  46075  fourierdlem104  46187  sqwvfoura  46205  sqwvfourb  46206  fzopredsuc  47300  fppr2odd  47693  dfnbgr5  47812  gpgprismgr4cycllem10  48051  rngccatidALTV  48195  ringccatidALTV  48229  0dig2pr01  48538  nn0sumshdiglemB  48548  imaidfu2  49018  oppczeroo  49102  dfswapf2  49126  prcof1  49246  setc1onsubc  49427