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 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 2708

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

This theorem is referenced by:  rabsnif  4667  uniintsn  4927  iinvdif  5022  iununi  5041  dmxpid  5885  rnxpid  6137  csbrn  6167  dmsnsnsn  6184  opswap  6193  xpcoid  6254  predres  6303  unizlim  6447  fvco4i  6941  fndmdifcom  6995  fmptsng  7123  fmptsnd  7124  csbov  7412  ordunisuc  7783  offres  7936  1stval2  7959  2ndval2  7960  cnvf1olem  8060  fparlem3  8064  fparlem4  8065  frrlem12  8247  seqomlem1  8389  ecovcom  8770  ecovass  8771  ecovdi  8772  resixpfo  8884  mapunen  9084  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  11326  indval2  12164  zeo  12615  xnegneg  13166  xaddcom  13192  xaddrid  13193  xnegdi  13200  xmulrid  13231  xadddilem  13246  ixxin  13315  fzsuc2  13536  expneg  14031  sq01  14187  facp1  14240  bcpasc  14283  hashfzp1  14393  resunimafz0  14407  hashf1lem1  14417  hashf1  14419  ccat1st1st  14591  swrdccatin1  14687  swrdccat3blem  14701  repswsymballbi  14742  cshwmodn  14757  cshwlen  14761  repswcshw  14774  trclun  14976  relexpcnv  14997  relexpaddd  15016  absexp  15266  sqreulem  15322  fsumf1o  15685  fsumadd  15702  fsumrev2  15744  fsumparts  15769  fsumrelem  15770  fprodf1o  15911  fprodmul  15925  fproddiv  15926  fprodfac  15938  fallfacfwd  16001  efexp  16068  tanval2  16100  sadeq  16441  smumullem  16461  smumul  16462  gcdcom  16482  gcd0id  16488  gcdass  16516  nn0expgcd  16533  lcmcom  16562  lcmneg  16572  lcmass  16583  nn0gcdsq  16722  dfphi2  16744  pcneg  16845  setscom  17150  strfvi  17160  fveqprc  17161  oveqprc  17162  ressbas  17206  ressinbas  17215  ressress  17217  firest  17395  topnval  17397  xpsfeq  17527  xpsaddlem  17537  xpsvsca  17541  oppchomfval  17680  rescbas  17796  rescco  17799  cofuass  17856  fucbas  17930  fuchom  17931  setccatid  18051  estrccatid  18098  xpcbas  18144  oduleval  18255  odulub  18371  oduglb  18373  ipotset  18499  efmndbas  18839  efmndbasabf  18840  symggrplem  18852  smndex1mndlem  18880  pwmnd  18908  grpinvfvi  18958  cntrval  19294  cntzval  19296  oppgplusfval  19323  snsymgefmndeq  19370  symgvalstruct  19372  pmtrprfval  19462  m1expaddsub  19473  sylow1lem2  19574  sylow3lem1  19602  oppglsm  19617  gsumzsplit  19902  gsum2dlem2  19946  gsumcom2  19950  dprd2dlem2  20017  dprd2da  20019  dmdprdsplit2lem  20022  mgpplusg  20125  mgpress  20131  ringidval  20164  opprmulfval  20319  abvtrivd  20809  sralem  21171  srasca  21175  sravsca  21176  sraip  21177  rlmval  21186  zlmsca  21500  zlmvsca  21501  psgninv  21562  ocvval  21647  thlbas  21676  thlle  21677  thloc  21679  dsmmval2  21716  psrmulr  21921  mplmonmul  22014  mplcoe3  22016  opsrbaslem  22027  opsrtoslem2  22034  psr1val  22149  ply1basfvi  22204  ply1plusgfvi  22205  psr1sca2  22214  evl1fval1lem  22295  mattpos1  22421  mdettpos  22576  smadiadetglem1  22636  tgdif0  22957  indislem  22965  restco  23129  txtopon  23556  txindislem  23598  qtopres  23663  hmphindis  23762  ptuncnv  23772  snclseqg  24081  tsmssplit  24117  ussval  24224  tuslem  24231  setsmsbas  24440  tngds  24613  tngtset  24614  pcoass  24991  cphsqrtcl2  25153  rrxcph  25359  ovolunlem1a  25463  ioorinv  25543  itg11  25658  itg1mulc  25671  itg2cnlem1  25728  iblss2  25773  ibladdlem  25787  itgfsum  25794  iblabslem  25795  iblabs  25796  ditgneg  25824  deg1fvi  26050  dgrco  26240  logfac  26565  cxpexp  26632  cxpmul2  26653  cxpsqrt  26667  cxpsqrtth  26694  dvcxp1  26704  dvcxp2  26705  ang180lem1  26773  mcubic  26811  quart1  26820  reasinsin  26860  atanlogaddlem  26877  atantayl2  26902  log2tlbnd  26909  basellem2  27045  basellem3  27046  basellem5  27048  basellem8  27051  fsumdvdsmul  27158  dchrmullid  27215  bcp1ctr  27242  lgsneg  27284  lgsneg1  27285  lgsdir2  27293  lgsdir  27295  lgsdi  27297  lgsquad2lem2  27348  pntleml  27574  lrold  27889  abssnid  28235  om2noseqfo  28290  n0seo  28413  pw2cutp1  28453  motgrp  28611  lmiisolem  28864  egrsubgr  29346  iswwlksnon  29921  iswspthsnon  29924  bafval  30675  ipidsq  30781  ipasslem1  30902  pjclem2  32267  cvmdi  32395  imadifxp  32671  2ndimaxp  32719  suppun2  32757  iundisjcnt  32871  dpfrac1  32951  gsumpart  33124  suppgsumssiun  33133  cycpmco2rn  33186  cyc3genpmlem  33212  fracbas  33366  resvsca  33392  psrgsum  33692  psrmonmul  33694  psrmonprod  33696  rspectset  34010  bayesth  34583  ofcccat  34687  plymulx  34692  subfacp1lem6  35367  satfdm  35551  mvtval  35682  mexval  35684  mexval2  35685  mdvval  35686  mrsubfval  35690  mrsubvrs  35704  msubfval  35706  elmsubrn  35710  mvhfval  35715  mpstval  35717  msrfval  35719  mstaval  35726  mthmval  35757  bccolsum  35921  dfrdg2  35975  dfrdg3  35976  dfrdg4  36133  ordtoplem  36617  ordcmp  36629  curunc  37923  matunitlindflem2  37938  poimirlem6  37947  poimirlem7  37948  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem16  37957  poimirlem19  37960  poimirlem21  37962  poimirlem22  37963  poimirlem27  37968  poimirlem31  37972  poimirlem32  37973  itg2addnclem2  37993  ibladdnclem  37997  iblabsnclem  38004  iblabsnc  38005  iblmulc2nc  38006  ftc1anclem8  38021  pmodN  40296  tgrpgrplem  41195  tendoplass  41229  tendoicl  41242  erngdvlem3  41436  dvhvaddass  41543  dib0  41610  dib1dim2  41614  diclspsn  41640  cdlemn8  41650  dihopelvalcpre  41694  djhcom  41851  evlsbagval  43002  kelac2  43493  mendbas  43608  mendring  43616  iscard4  43960  relexp01min  44140  relexpaddss  44145  iotain  44844  addrcom  44901  rnsnf  45614  itgsinexplem1  46382  volioc  46400  dirkertrigeqlem1  46526  fourierdlem104  46638  sqwvfoura  46656  sqwvfourb  46657  hoicvr  46976  fzopredsuc  47772  ppivalnn  48095  fppr2odd  48207  dfnbgr5  48327  gpgprismgr4cycllem10  48580  rngccatidALTV  48748  ringccatidALTV  48782  0dig2pr01  49086  nn0sumshdiglemB  49096  imaidfu2  49586  oppczeroo  49712  dfswapf2  49736  oppc1stf  49763  oppc2ndf  49764  prcof1  49863  setc1onsubc  50077  termolmd  50145