Theorem 3eqtr4a 2790

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 2780	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2767	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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  rabsnif  4687  uniintsn  4949  iinvdif  5044  iununi  5063  dmxpid  5894  rnxpid  6146  csbrn  6176  dmsnsnsn  6193  opswap  6202  xpcoid  6263  predres  6312  unizlim  6457  fvco4i  6962  fndmdifcom  7015  fmptsng  7142  fmptsnd  7143  csbov  7432  ordunisuc  7807  offres  7962  1stval2  7985  2ndval2  7986  cnvf1olem  8089  fparlem3  8093  fparlem4  8094  frrlem12  8276  seqomlem1  8418  ecovcom  8796  ecovass  8797  ecovdi  8798  resixpfo  8909  mapunen  9110  cardidm  9912  cardiun  9935  alephcard  10023  cardalephex  10043  cardcf  10205  cfidm  10228  alephsing  10229  itunisuc  10372  itunitc  10374  ituniiun  10375  alephadd  10530  alephreg  10535  pwcfsdom  10536  addcompq  10903  addcomnq  10904  mulcompq  10905  mulcomnq  10906  addassnq  10911  mulassnq  10912  addrid  11354  zeo  12620  xnegneg  13174  xaddcom  13200  xaddrid  13201  xnegdi  13208  xmulrid  13239  xadddilem  13254  ixxin  13323  fzsuc2  13543  expneg  14034  sq01  14190  facp1  14243  bcpasc  14286  hashfzp1  14396  resunimafz0  14410  hashf1lem1  14420  hashf1  14422  ccat1st1st  14593  swrdccatin1  14690  swrdccat3blem  14704  repswsymballbi  14745  cshwmodn  14760  cshwlen  14764  repswcshw  14777  trclun  14980  relexpcnv  15001  relexpaddd  15020  absexp  15270  sqreulem  15326  fsumf1o  15689  fsumadd  15706  fsumrev2  15748  fsumparts  15772  fsumrelem  15773  fprodf1o  15912  fprodmul  15926  fproddiv  15927  fprodfac  15939  fallfacfwd  16002  efexp  16069  tanval2  16101  sadeq  16442  smumullem  16462  smumul  16463  gcdcom  16483  gcd0id  16489  gcdass  16517  nn0expgcd  16534  lcmcom  16563  lcmneg  16573  lcmass  16584  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  17526  xpsaddlem  17536  xpsvsca  17540  oppchomfval  17675  rescbas  17791  rescco  17794  cofuass  17851  fucbas  17925  fuchom  17926  setccatid  18046  estrccatid  18093  xpcbas  18139  oduleval  18250  odulub  18366  oduglb  18368  ipotset  18492  efmndbas  18798  efmndbasabf  18799  symggrplem  18811  smndex1mndlem  18836  pwmnd  18864  grpinvfvi  18914  cntrval  19251  cntzval  19253  oppgplusfval  19280  snsymgefmndeq  19325  symgvalstruct  19327  pmtrprfval  19417  m1expaddsub  19428  sylow1lem2  19529  sylow3lem1  19557  oppglsm  19572  gsumzsplit  19857  gsum2dlem2  19901  gsumcom2  19905  dprd2dlem2  19972  dprd2da  19974  dmdprdsplit2lem  19977  mgpplusg  20053  mgpress  20059  ringidval  20092  opprmulfval  20248  abvtrivd  20741  sralem  21083  srasca  21087  sravsca  21088  sraip  21089  rlmval  21098  zlmsca  21430  zlmvsca  21431  psgninv  21491  ocvval  21576  thlbas  21605  thlle  21606  thloc  21608  dsmmval2  21645  psrmulr  21851  mplmonmul  21943  mplcoe3  21945  opsrbaslem  21956  opsrtoslem2  21963  psr1val  22070  ply1basfvi  22125  ply1plusgfvi  22126  psr1sca2  22135  evl1fval1lem  22217  mattpos1  22343  mdettpos  22498  smadiadetglem1  22558  tgdif0  22879  indislem  22887  restco  23051  txtopon  23478  txindislem  23520  qtopres  23585  hmphindis  23684  ptuncnv  23694  snclseqg  24003  tsmssplit  24039  ussval  24147  tuslem  24154  setsmsbas  24363  tngds  24536  tngtset  24537  pcoass  24924  cphsqrtcl2  25086  rrxcph  25292  ovolunlem1a  25397  ioorinv  25477  itg11  25592  itg1mulc  25605  itg2cnlem1  25662  iblss2  25707  ibladdlem  25721  itgfsum  25728  iblabslem  25729  iblabs  25730  ditgneg  25758  deg1fvi  25990  dgrco  26181  logfac  26510  cxpexp  26577  cxpmul2  26598  cxpsqrt  26612  cxpsqrtth  26639  dvcxp1  26649  dvcxp2  26650  ang180lem1  26719  mcubic  26757  quart1  26766  reasinsin  26806  atanlogaddlem  26823  atantayl2  26848  log2tlbnd  26855  basellem2  26992  basellem3  26993  basellem5  26995  basellem8  26998  fsumdvdsmul  27105  dchrmullid  27163  bcp1ctr  27190  lgsneg  27232  lgsneg1  27233  lgsdir2  27241  lgsdir  27243  lgsdi  27245  lgsquad2lem2  27296  pntleml  27522  lrold  27808  abssnid  28145  om2noseqfo  28192  n0seo  28307  pw2cutp1  28336  zs12bday  28343  motgrp  28470  lmiisolem  28723  egrsubgr  29204  iswwlksnon  29783  iswspthsnon  29786  bafval  30533  ipidsq  30639  ipasslem1  30760  pjclem2  32125  cvmdi  32253  imadifxp  32530  2ndimaxp  32570  suppun2  32607  iundisjcnt  32721  indval2  32777  dpfrac1  32812  gsumpart  32997  cycpmco2rn  33082  cyc3genpmlem  33108  fracbas  33255  resvsca  33304  rspectset  33856  bayesth  34430  ofcccat  34534  plymulx  34539  subfacp1lem6  35172  satfdm  35356  mvtval  35487  mexval  35489  mexval2  35490  mdvval  35491  mrsubfval  35495  mrsubvrs  35509  msubfval  35511  elmsubrn  35515  mvhfval  35520  mpstval  35522  msrfval  35524  mstaval  35531  mthmval  35562  bccolsum  35726  dfrdg2  35783  dfrdg3  35784  dfrdg4  35939  ordtoplem  36423  ordcmp  36435  curunc  37596  matunitlindflem2  37611  poimirlem6  37620  poimirlem7  37621  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem16  37630  poimirlem19  37633  poimirlem21  37635  poimirlem22  37636  poimirlem27  37641  poimirlem31  37645  poimirlem32  37646  itg2addnclem2  37666  ibladdnclem  37670  iblabsnclem  37677  iblabsnc  37678  iblmulc2nc  37679  ftc1anclem8  37694  pmodN  39844  tgrpgrplem  40743  tendoplass  40777  tendoicl  40790  erngdvlem3  40984  dvhvaddass  41091  dib0  41158  dib1dim2  41162  diclspsn  41188  cdlemn8  41198  dihopelvalcpre  41242  djhcom  41399  evlsbagval  42554  kelac2  43054  mendbas  43169  mendring  43177  iscard4  43522  relexp01min  43702  relexpaddss  43707  iotain  44406  addrcom  44464  rnsnf  45178  itgsinexplem1  45952  volioc  45970  dirkertrigeqlem1  46096  fourierdlem104  46208  sqwvfoura  46226  sqwvfourb  46227  fzopredsuc  47324  fppr2odd  47732  dfnbgr5  47851  gpgprismgr4cycllem10  48094  rngccatidALTV  48260  ringccatidALTV  48294  0dig2pr01  48599  nn0sumshdiglemB  48609  imaidfu2  49100  oppczeroo  49226  dfswapf2  49250  oppc1stf  49277  oppc2ndf  49278  prcof1  49377  setc1onsubc  49591  termolmd  49659