Theorem 3eqtr4a 2864

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

Syntax hints:   → wi 4   = wceq 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2782

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2797

This theorem is referenced by:  rabsnif  4447  uniintsn  4704  iinvdif  4782  iununi  4800  dmxpid  5544  rnxpid  5776  csbrn  5805  dmsnsnsn  5823  opswap  5834  xpcoid  5888  unizlim  6055  fvco4i  6495  fndmdifcom  6542  fmptsng  6657  fmptsnd  6658  csbov  6914  ordunisuc  7260  offres  7391  1stval2  7413  2ndval2  7414  cnvf1olem  7507  fparlem3  7511  fparlem4  7512  imacosupp  7568  seqomlem1  7779  ecovcom  8087  ecovass  8088  ecovdi  8089  resixpfo  8181  mapunen  8366  cardidm  9066  cardiun  9089  alephcard  9174  cardalephex  9194  cardcf  9357  cfidm  9380  alephsing  9381  itunisuc  9524  itunitc  9526  ituniiun  9527  alephadd  9682  alephreg  9687  pwcfsdom  9688  addcompq  10055  addcomnq  10056  mulcompq  10057  mulcomnq  10058  addassnq  10063  mulassnq  10064  addid1  10499  zeo  11727  xnegneg  12261  xaddcom  12287  xaddid1  12288  xnegdi  12294  xmulid1  12325  xadddilem  12340  ixxin  12408  fzsuc2  12619  expneg  13089  sq01  13207  facp1  13283  bcpasc  13326  hashfzp1  13433  resunimafz0  13444  hashf1lem1  13454  hashf1  13456  ccat1st1st  13624  swrdccatin1  13705  swrdccat3blem  13717  repswsymballbi  13749  cshwmodn  13763  repswcshw  13780  trclun  13976  relexpcnv  13996  absexp  14265  sqreulem  14320  fsumf1o  14675  fsumadd  14691  fsumrev2  14734  fsumparts  14758  fsumrelem  14759  pwm1geoser  14820  fprodf1o  14895  fprodmul  14909  fproddiv  14910  fprodfac  14922  fallfacfwd  14985  efexp  15049  tanval2  15081  sqrt2irrlemOLD  15196  sadeq  15411  smumullem  15431  smumul  15432  gcdcom  15452  gcd0id  15457  gcdass  15481  lcmcom  15523  lcmneg  15533  lcmass  15544  nn0gcdsq  15675  dfphi2  15694  pcneg  15793  setscom  16112  strfvi  16122  setsnid  16124  ressbas  16139  ressinbas  16145  ressress  16148  firest  16296  topnval  16298  xpsfeq  16427  xpsaddlem  16438  xpsvsca  16442  homffval  16552  oppchomfval  16576  oppcbas  16580  rescbas  16691  rescco  16694  cofuass  16751  fucbas  16822  fuchom  16823  setccatid  16936  estrccatid  16974  xpcbas  17021  xpchomfval  17022  xpccofval  17025  oduleval  17334  oduglb  17342  odulub  17344  ipotset  17360  grpinvfvi  17666  cntrval  17951  cntzval  17953  oppgplusfval  17977  symgbas  17999  symggrp  18019  pmtrprfval  18106  m1expaddsub  18117  sylow1lem2  18213  sylow3lem1  18241  oppglsm  18256  gsumzsplit  18526  gsum2dlem2  18569  gsumcom2  18573  dprd2dlem2  18639  dprd2da  18641  dmdprdsplit2lem  18644  mgpplusg  18693  mgpress  18700  ringidval  18703  opprmulfval  18825  abvtrivd  19042  sralem  19384  srasca  19388  sravsca  19389  sraip  19390  rlmval  19398  psrmulr  19591  mplmonmul  19671  mplcoe3  19673  opsrbaslem  19684  opsrtoslem2  19691  psr1val  19762  ply1basfvi  19817  ply1plusgfvi  19818  psr1sca2  19827  evl1fval1lem  19900  zlmlem  20071  zlmsca  20075  zlmvsca  20076  psgninv  20133  ocvval  20219  thlbas  20248  thlle  20249  thloc  20251  dsmmval2  20288  mattpos1  20471  mdettpos  20626  smadiadetglem1  20687  tgdif0  21008  indislem  21016  restco  21180  txtopon  21606  txindislem  21648  qtopres  21713  hmphindis  21812  ptuncnv  21822  snclseqg  22130  tsmssplit  22166  ussval  22274  tuslem  22282  setsmsbas  22491  tnglem  22655  tngds  22663  tngtset  22664  pcoass  23034  cphsqrtcl2  23196  rrxcph  23390  ovolunlem1a  23475  ioorinv  23555  itg11  23670  itg1mulc  23683  itg2cnlem1  23740  iblss2  23784  ibladdlem  23798  itgfsum  23805  iblabslem  23806  iblabs  23807  ditgneg  23833  deg1fvi  24057  dgrco  24243  logfac  24559  cxpexp  24626  cxpmul2  24647  cxpsqrt  24661  dvcxp1  24693  dvcxp2  24694  ang180lem1  24751  mcubic  24786  quart1  24795  reasinsin  24835  atanlogaddlem  24852  atantayl2  24877  log2tlbnd  24884  basellem2  25020  basellem3  25021  basellem5  25023  basellem8  25026  dchrmulid2  25189  bcp1ctr  25216  lgsneg  25258  lgsneg1  25259  lgsdir2  25267  lgsdir  25269  lgsdi  25271  lgsquad2lem2  25322  pntleml  25512  motgrp  25650  lmiisolem  25900  ttglem  25968  egrsubgr  26383  iswwlksnon  26973  iswwlksnonOLD  26974  iswspthsnon  26977  iswspthsnonOLD  26978  bafval  27785  ipidsq  27891  ipasslem1  28012  pjclem2  29381  cvmdi  29509  imadifxp  29737  iundisjcnt  29882  dpfrac1  29923  resvsca  30153  indval2  30399  bayesth  30824  plymulx  30948  subfacp1lem6  31488  mvtval  31718  mexval  31720  mexval2  31721  mdvval  31722  mrsubfval  31726  mrsubvrs  31740  msubfval  31742  elmsubrn  31746  mvhfval  31751  mpstval  31753  msrfval  31755  mstaval  31762  mthmval  31793  bccolsum  31945  dfrdg2  32019  dfrdg3  32020  dfrdg4  32377  ordtoplem  32749  ordcmp  32761  curunc  33702  matunitlindflem2  33717  poimirlem6  33726  poimirlem7  33727  poimirlem11  33731  poimirlem12  33732  poimirlem13  33733  poimirlem14  33734  poimirlem16  33736  poimirlem19  33739  poimirlem21  33741  poimirlem22  33742  poimirlem27  33747  poimirlem31  33751  poimirlem32  33752  itg2addnclem2  33772  ibladdnclem  33776  iblabsnclem  33783  iblabsnc  33784  iblmulc2nc  33785  ftc1anclem8  33802  pmodN  35628  tgrpgrplem  36528  tendoplass  36562  tendoicl  36575  erngdvlem3  36769  dvhvaddass  36876  dib0  36943  dib1dim2  36947  diclspsn  36973  cdlemn8  36983  dihopelvalcpre  37027  djhcom  37184  kelac2  38134  mendbas  38253  mendsca  38258  mendring  38261  relexp01min  38503  relexpaddss  38508  iotain  39115  addrcom  39175  itgsinexplem1  40647  volioc  40665  dirkertrigeqlem1  40792  fourierdlem104  40904  sqwvfoura  40922  sqwvfourb  40923  fzopredsuc  41906  rngccatidALTV  42555  ringccatidALTV  42618  0dig2pr01  42970  nn0sumshdiglemB  42980