Theorem 3eqtr4a 2798

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 2788	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2775	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  rabsnif  4682  uniintsn  4942  iinvdif  5037  iununi  5056  dmxpid  5887  rnxpid  6139  csbrn  6169  dmsnsnsn  6186  opswap  6195  xpcoid  6256  predres  6305  unizlim  6449  fvco4i  6943  fndmdifcom  6997  fmptsng  7124  fmptsnd  7125  csbov  7413  ordunisuc  7784  offres  7937  1stval2  7960  2ndval2  7961  cnvf1olem  8062  fparlem3  8066  fparlem4  8067  frrlem12  8249  seqomlem1  8391  ecovcom  8772  ecovass  8773  ecovdi  8774  resixpfo  8886  mapunen  9086  cardidm  9883  cardiun  9906  alephcard  9992  cardalephex  10012  cardcf  10174  cfidm  10197  alephsing  10198  itunisuc  10341  itunitc  10343  ituniiun  10344  alephadd  10500  alephreg  10505  pwcfsdom  10506  addcompq  10873  addcomnq  10874  mulcompq  10875  mulcomnq  10876  addassnq  10881  mulassnq  10882  addrid  11325  zeo  12590  xnegneg  13141  xaddcom  13167  xaddrid  13168  xnegdi  13175  xmulrid  13206  xadddilem  13221  ixxin  13290  fzsuc2  13510  expneg  14004  sq01  14160  facp1  14213  bcpasc  14256  hashfzp1  14366  resunimafz0  14380  hashf1lem1  14390  hashf1  14392  ccat1st1st  14564  swrdccatin1  14660  swrdccat3blem  14674  repswsymballbi  14715  cshwmodn  14730  cshwlen  14734  repswcshw  14747  trclun  14949  relexpcnv  14970  relexpaddd  14989  absexp  15239  sqreulem  15295  fsumf1o  15658  fsumadd  15675  fsumrev2  15717  fsumparts  15741  fsumrelem  15742  fprodf1o  15881  fprodmul  15895  fproddiv  15896  fprodfac  15908  fallfacfwd  15971  efexp  16038  tanval2  16070  sadeq  16411  smumullem  16431  smumul  16432  gcdcom  16452  gcd0id  16458  gcdass  16486  nn0expgcd  16503  lcmcom  16532  lcmneg  16542  lcmass  16553  nn0gcdsq  16691  dfphi2  16713  pcneg  16814  setscom  17119  strfvi  17129  fveqprc  17130  oveqprc  17131  ressbas  17175  ressinbas  17184  ressress  17186  firest  17364  topnval  17366  xpsfeq  17496  xpsaddlem  17506  xpsvsca  17510  oppchomfval  17649  rescbas  17765  rescco  17768  cofuass  17825  fucbas  17899  fuchom  17900  setccatid  18020  estrccatid  18067  xpcbas  18113  oduleval  18224  odulub  18340  oduglb  18342  ipotset  18468  efmndbas  18808  efmndbasabf  18809  symggrplem  18821  smndex1mndlem  18846  pwmnd  18874  grpinvfvi  18924  cntrval  19260  cntzval  19262  oppgplusfval  19289  snsymgefmndeq  19336  symgvalstruct  19338  pmtrprfval  19428  m1expaddsub  19439  sylow1lem2  19540  sylow3lem1  19568  oppglsm  19583  gsumzsplit  19868  gsum2dlem2  19912  gsumcom2  19916  dprd2dlem2  19983  dprd2da  19985  dmdprdsplit2lem  19988  mgpplusg  20091  mgpress  20097  ringidval  20130  opprmulfval  20287  abvtrivd  20777  sralem  21140  srasca  21144  sravsca  21145  sraip  21146  rlmval  21155  zlmsca  21487  zlmvsca  21488  psgninv  21549  ocvval  21634  thlbas  21663  thlle  21664  thloc  21666  dsmmval2  21703  psrmulr  21910  mplmonmul  22003  mplcoe3  22005  opsrbaslem  22016  opsrtoslem2  22023  psr1val  22138  ply1basfvi  22193  ply1plusgfvi  22194  psr1sca2  22203  evl1fval1lem  22286  mattpos1  22412  mdettpos  22567  smadiadetglem1  22627  tgdif0  22948  indislem  22956  restco  23120  txtopon  23547  txindislem  23589  qtopres  23654  hmphindis  23753  ptuncnv  23763  snclseqg  24072  tsmssplit  24108  ussval  24215  tuslem  24222  setsmsbas  24431  tngds  24604  tngtset  24605  pcoass  24992  cphsqrtcl2  25154  rrxcph  25360  ovolunlem1a  25465  ioorinv  25545  itg11  25660  itg1mulc  25673  itg2cnlem1  25730  iblss2  25775  ibladdlem  25789  itgfsum  25796  iblabslem  25797  iblabs  25798  ditgneg  25826  deg1fvi  26058  dgrco  26249  logfac  26578  cxpexp  26645  cxpmul2  26666  cxpsqrt  26680  cxpsqrtth  26707  dvcxp1  26717  dvcxp2  26718  ang180lem1  26787  mcubic  26825  quart1  26834  reasinsin  26874  atanlogaddlem  26891  atantayl2  26916  log2tlbnd  26923  basellem2  27060  basellem3  27061  basellem5  27063  basellem8  27066  fsumdvdsmul  27173  dchrmullid  27231  bcp1ctr  27258  lgsneg  27300  lgsneg1  27301  lgsdir2  27309  lgsdir  27311  lgsdi  27313  lgsquad2lem2  27364  pntleml  27590  lrold  27905  abssnid  28251  om2noseqfo  28306  n0seo  28429  pw2cutp1  28469  motgrp  28627  lmiisolem  28880  egrsubgr  29362  iswwlksnon  29938  iswspthsnon  29941  bafval  30692  ipidsq  30798  ipasslem1  30919  pjclem2  32284  cvmdi  32412  imadifxp  32688  2ndimaxp  32736  suppun2  32774  iundisjcnt  32889  indval2  32944  dpfrac1  32984  gsumpart  33157  suppgsumssiun  33166  cycpmco2rn  33219  cyc3genpmlem  33245  fracbas  33399  resvsca  33425  psrgsum  33725  psrmonmul  33727  psrmonprod  33729  rspectset  34044  bayesth  34617  ofcccat  34721  plymulx  34726  subfacp1lem6  35401  satfdm  35585  mvtval  35716  mexval  35718  mexval2  35719  mdvval  35720  mrsubfval  35724  mrsubvrs  35738  msubfval  35740  elmsubrn  35744  mvhfval  35749  mpstval  35751  msrfval  35753  mstaval  35760  mthmval  35791  bccolsum  35955  dfrdg2  36009  dfrdg3  36010  dfrdg4  36167  ordtoplem  36651  ordcmp  36663  curunc  37853  matunitlindflem2  37868  poimirlem6  37877  poimirlem7  37878  poimirlem11  37882  poimirlem12  37883  poimirlem13  37884  poimirlem14  37885  poimirlem16  37887  poimirlem19  37890  poimirlem21  37892  poimirlem22  37893  poimirlem27  37898  poimirlem31  37902  poimirlem32  37903  itg2addnclem2  37923  ibladdnclem  37927  iblabsnclem  37934  iblabsnc  37935  iblmulc2nc  37936  ftc1anclem8  37951  pmodN  40226  tgrpgrplem  41125  tendoplass  41159  tendoicl  41172  erngdvlem3  41366  dvhvaddass  41473  dib0  41540  dib1dim2  41544  diclspsn  41570  cdlemn8  41580  dihopelvalcpre  41624  djhcom  41781  evlsbagval  42927  kelac2  43422  mendbas  43537  mendring  43545  iscard4  43889  relexp01min  44069  relexpaddss  44074  iotain  44773  addrcom  44830  rnsnf  45543  itgsinexplem1  46312  volioc  46330  dirkertrigeqlem1  46456  fourierdlem104  46568  sqwvfoura  46586  sqwvfourb  46587  fzopredsuc  47683  fppr2odd  48091  dfnbgr5  48211  gpgprismgr4cycllem10  48464  rngccatidALTV  48632  ringccatidALTV  48666  0dig2pr01  48970  nn0sumshdiglemB  48980  imaidfu2  49470  oppczeroo  49596  dfswapf2  49620  oppc1stf  49647  oppc2ndf  49648  prcof1  49747  setc1onsubc  49961  termolmd  50029