Theorem 3eqtr4a 2806

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 2796	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2783	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 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  rabsnif  4665  uniintsn  4924  iinvdif  5014  iununi  5033  dmxpid  5838  rnxpid  6075  csbrn  6105  dmsnsnsn  6122  opswap  6131  xpcoid  6192  predres  6241  unizlim  6382  fvco4i  6866  fndmdifcom  6917  fmptsng  7037  fmptsnd  7038  csbov  7314  ordunisuc  7673  offres  7819  1stval2  7841  2ndval2  7842  cnvf1olem  7941  fparlem3  7945  fparlem4  7946  frrlem12  8104  seqomlem1  8272  ecovcom  8595  ecovass  8596  ecovdi  8597  resixpfo  8707  mapunen  8915  cardidm  9718  cardiun  9741  alephcard  9827  cardalephex  9847  cardcf  10009  cfidm  10032  alephsing  10033  itunisuc  10176  itunitc  10178  ituniiun  10179  alephadd  10334  alephreg  10339  pwcfsdom  10340  addcompq  10707  addcomnq  10708  mulcompq  10709  mulcomnq  10710  addassnq  10715  mulassnq  10716  addid1  11155  zeo  12406  xnegneg  12947  xaddcom  12973  xaddid1  12974  xnegdi  12981  xmulid1  13012  xadddilem  13027  ixxin  13095  fzsuc2  13313  expneg  13788  sq01  13938  facp1  13990  bcpasc  14033  hashfzp1  14144  resunimafz0  14155  hashf1lem1  14166  hashf1lem1OLD  14167  hashf1  14169  ccat1st1st  14333  swrdccatin1  14436  swrdccat3blem  14450  repswsymballbi  14491  cshwmodn  14506  cshwlen  14510  repswcshw  14523  trclun  14723  relexpcnv  14744  relexpaddd  14763  absexp  15014  sqreulem  15069  fsumf1o  15433  fsumadd  15450  fsumrev2  15492  fsumparts  15516  fsumrelem  15517  fprodf1o  15654  fprodmul  15668  fproddiv  15669  fprodfac  15681  fallfacfwd  15744  efexp  15808  tanval2  15840  sadeq  16177  smumullem  16197  smumul  16198  gcdcom  16218  gcd0id  16224  gcdass  16253  lcmcom  16296  lcmneg  16306  lcmass  16317  nn0gcdsq  16454  dfphi2  16473  pcneg  16573  setscom  16879  strfvi  16889  fveqprc  16890  oveqprc  16891  setsnidOLD  16909  ressbas  16945  ressbasOLD  16946  ressinbas  16953  ressress  16956  firest  17141  topnval  17143  xpsfeq  17272  xpsaddlem  17282  xpsvsca  17286  oppchomfval  17421  oppchomfvalOLD  17422  oppcbasOLD  17427  rescbas  17539  rescbasOLD  17540  rescco  17543  resccoOLD  17544  cofuass  17602  fucbas  17675  fuchom  17676  fuchomOLD  17677  setccatid  17797  estrccatid  17846  xpcbas  17893  oduleval  18005  odulub  18123  oduglb  18125  ipotset  18249  efmndbas  18508  efmndbasabf  18509  symggrplem  18521  smndex1mndlem  18546  pwmnd  18574  grpinvfvi  18620  cntrval  18923  cntzval  18925  oppgplusfval  18950  snsymgefmndeq  19000  symgvalstruct  19002  symgvalstructOLD  19003  pmtrprfval  19093  m1expaddsub  19104  sylow1lem2  19202  sylow3lem1  19230  oppglsm  19245  gsumzsplit  19526  gsum2dlem2  19570  gsumcom2  19574  dprd2dlem2  19641  dprd2da  19643  dmdprdsplit2lem  19646  mgpplusg  19722  mgpress  19733  mgpressOLD  19734  ringidval  19737  opprmulfval  19862  abvtrivd  20098  sralem  20437  sralemOLD  20438  srasca  20445  srascaOLD  20446  sravsca  20447  sravscaOLD  20448  sraip  20449  rlmval  20459  zlmlemOLD  20717  zlmsca  20724  zlmvsca  20725  psgninv  20785  ocvval  20870  thlbas  20899  thlbasOLD  20900  thlle  20901  thlleOLD  20902  thloc  20904  dsmmval2  20941  psrmulr  21151  mplmonmul  21235  mplcoe3  21237  opsrbaslem  21248  opsrbaslemOLD  21249  opsrtoslem2  21261  psr1val  21355  ply1basfvi  21410  ply1plusgfvi  21411  psr1sca2  21420  evl1fval1lem  21494  mattpos1  21603  mdettpos  21758  smadiadetglem1  21818  tgdif0  22140  indislem  22148  restco  22313  txtopon  22740  txindislem  22782  qtopres  22847  hmphindis  22946  ptuncnv  22956  snclseqg  23265  tsmssplit  23301  ussval  23409  tuslem  23416  tuslemOLD  23417  setsmsbas  23626  setsmsbasOLD  23627  tnglemOLD  23795  tngds  23809  tngdsOLD  23810  tngtset  23811  pcoass  24185  cphsqrtcl2  24348  rrxcph  24554  ovolunlem1a  24658  ioorinv  24738  itg11  24853  itg1mulc  24867  itg2cnlem1  24924  iblss2  24968  ibladdlem  24982  itgfsum  24989  iblabslem  24990  iblabs  24991  ditgneg  25019  deg1fvi  25248  dgrco  25434  logfac  25754  cxpexp  25821  cxpmul2  25842  cxpsqrt  25856  cxpsqrtth  25882  dvcxp1  25891  dvcxp2  25892  ang180lem1  25957  mcubic  25995  quart1  26004  reasinsin  26044  atanlogaddlem  26061  atantayl2  26086  log2tlbnd  26093  basellem2  26229  basellem3  26230  basellem5  26232  basellem8  26235  dchrmulid2  26398  bcp1ctr  26425  lgsneg  26467  lgsneg1  26468  lgsdir2  26476  lgsdir  26478  lgsdi  26480  lgsquad2lem2  26531  pntleml  26757  motgrp  26902  lmiisolem  27155  ttglemOLD  27237  egrsubgr  27642  iswwlksnon  28214  iswspthsnon  28217  bafval  28962  ipidsq  29068  ipasslem1  29189  pjclem2  30554  cvmdi  30682  imadifxp  30936  2ndimaxp  30980  iundisjcnt  31115  dpfrac1  31162  gsumpart  31311  cycpmco2rn  31388  cyc3genpmlem  31414  resvsca  31525  rspectset  31812  indval2  31978  bayesth  32402  ofcccat  32518  plymulx  32523  subfacp1lem6  33143  satfdm  33327  mvtval  33458  mexval  33460  mexval2  33461  mdvval  33462  mrsubfval  33466  mrsubvrs  33480  msubfval  33482  elmsubrn  33486  mvhfval  33491  mpstval  33493  msrfval  33495  mstaval  33502  mthmval  33533  bccolsum  33701  dfrdg2  33767  dfrdg3  33768  lrold  34073  dfrdg4  34249  ordtoplem  34620  ordcmp  34632  curunc  35755  matunitlindflem2  35770  poimirlem6  35779  poimirlem7  35780  poimirlem11  35784  poimirlem12  35785  poimirlem13  35786  poimirlem14  35787  poimirlem16  35789  poimirlem19  35792  poimirlem21  35794  poimirlem22  35795  poimirlem27  35800  poimirlem31  35804  poimirlem32  35805  itg2addnclem2  35825  ibladdnclem  35829  iblabsnclem  35836  iblabsnc  35837  iblmulc2nc  35838  ftc1anclem8  35853  pmodN  37860  tgrpgrplem  38759  tendoplass  38793  tendoicl  38806  erngdvlem3  39000  dvhvaddass  39107  dib0  39174  dib1dim2  39178  diclspsn  39204  cdlemn8  39214  dihopelvalcpre  39258  djhcom  39415  nn0expgcd  40332  kelac2  40887  mendbas  41006  mendring  41014  iscard4  41119  relexp01min  41291  relexpaddss  41296  iotain  42005  addrcom  42063  rnsnf  42691  itgsinexplem1  43466  volioc  43484  dirkertrigeqlem1  43610  fourierdlem104  43722  sqwvfoura  43740  sqwvfourb  43741  fzopredsuc  44784  fppr2odd  45152  rngccatidALTV  45516  ringccatidALTV  45579  0dig2pr01  45925  nn0sumshdiglemB  45935