Theorem 3eqtr4a 2830

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

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  rabsnif  4694  uniintsn  4954  iinvdif  5050  iununi  5069  csbcnv  5873  dmxpid  5921  rnxpid  6172  csbrn  6205  dmsnsnsn  6222  opswap  6231  xpcoid  6292  predres  6341  unizlim  6486  fvco4i  6984  fndmdifcom  7039  fmptsng  7167  fmptsnd  7168  csbov  7456  ordunisuc  7827  offres  7979  1stval2  8002  2ndval2  8003  cnvf1olem  8104  fparlem3  8108  fparlem4  8109  frrlem12  8293  seqomlem1  8436  ecovcom  8820  ecovass  8821  ecovdi  8822  resixpfo  8933  mapunen  9133  cardidm  9944  cardiun  9967  alephcard  10053  cardalephex  10073  cardcf  10234  cfidm  10258  alephsing  10259  itunisuc  10402  itunitc  10404  ituniiun  10405  alephadd  10561  alephreg  10566  pwcfsdom  10567  addcompq  10934  addcomnq  10935  mulcompq  10936  mulcomnq  10937  addassnq  10942  mulassnq  10943  addrid  11389  indval2  12222  zeo  12681  xnegneg  13239  xaddcom  13265  xaddrid  13266  xnegdi  13273  xmulrid  13304  xadddilem  13319  ixxin  13388  fzsuc2  13609  expneg  14104  sq01  14260  facp1  14313  bcpasc  14356  hashfzp1  14467  resunimafz0  14481  hashf1lem1  14491  hashf1  14493  ccat1st1st  14665  swrdccatin1  14761  swrdccat3blem  14775  repswsymballbi  14816  cshwmodn  14831  cshwlen  14835  repswcshw  14848  trclun  15050  relexpcnv  15071  relexpaddd  15090  absexp  15354  sqreulem  15410  fsumf1o  15773  fsumadd  15790  fsumrev2  15832  fsumparts  15857  fsumrelem  15858  fprodf1o  15999  fprodmul  16013  fproddiv  16014  fprodfac  16026  fallfacfwd  16089  efexp  16156  tanval2  16188  sadeq  16529  smumullem  16549  smumul  16550  gcdcom  16570  gcd0id  16576  gcdass  16604  nn0expgcd  16621  lcmcom  16650  lcmneg  16660  lcmass  16671  nn0gcdsq  16810  dfphi2  16832  pcneg  16933  setscom  17239  strfvi  17249  fveqprc  17250  oveqprc  17251  ressbas  17295  ressinbas  17304  ressress  17306  firest  17484  topnval  17486  xpsfeq  17616  xpsaddlem  17626  xpsvsca  17630  oppchomfval  17769  rescbas  17885  rescco  17888  cofuass  17945  fucbas  18019  fuchom  18020  setccatid  18140  estrccatid  18187  xpcbas  18233  oduleval  18344  odulub  18460  oduglb  18462  ipotset  18588  efmndbas  18929  efmndbasabf  18930  symggrplem  18942  smndex1mndlem  18970  pwmnd  18998  grpinvfvi  19048  cntrval  19388  cntzval  19390  oppgplusfval  19417  snsymgefmndeq  19464  symgvalstruct  19466  pmtrprfval  19556  m1expaddsub  19567  sylow1lem2  19668  sylow3lem1  19696  oppglsm  19711  gsumzsplit  19996  gsum2dlem2  20040  gsumcom2  20044  dprd2dlem2  20111  dprd2da  20113  dmdprdsplit2lem  20116  mgpplusg  20219  mgpress  20225  ringidval  20264  opprmulfval  20420  abvtrivd  20912  sralem  21274  srasca  21278  sravsca  21279  sraip  21280  rlmval  21289  zlmsca  21638  zlmvsca  21639  psgninv  21700  ocvval  21785  thlbas  21814  thlle  21815  thloc  21817  dsmmval2  21854  psrmulr  22060  mplmonmul  22155  mplcoe3  22157  opsrbaslem  22168  opsrtoslem2  22175  psr1val  22314  ply1basfvi  22368  ply1plusgfvi  22369  psr1sca2  22378  evl1fval1lem  22458  mattpos1  22581  mdettpos  22736  smadiadetglem1  22796  tgdif0  23117  indislem  23125  restco  23289  txtopon  23716  txindislem  23758  qtopres  23823  hmphindis  23922  ptuncnv  23932  snclseqg  24241  tsmssplit  24277  ussval  24384  tuslem  24391  setsmsbas  24600  tngds  24773  tngtset  24774  pcoass  25151  cphsqrtcl2  25313  rrxcph  25519  ovolunlem1a  25623  ioorinv  25703  itg11  25818  itg1mulc  25831  itg2cnlem1  25888  iblss2  25933  ibladdlem  25947  itgfsum  25954  iblabslem  25955  iblabs  25956  ditgneg  25984  deg1fvi  26210  dgrco  26400  plymulidp  26411  logfac  26731  cxpexp  26798  cxpmul2  26819  cxpsqrt  26833  cxpsqrtth  26860  dvcxp1  26870  dvcxp2  26871  ang180lem1  26939  mcubic  26977  quart1  26986  reasinsin  27026  atanlogaddlem  27043  atantayl2  27068  log2tlbnd  27075  basellem2  27211  basellem3  27212  basellem5  27214  basellem8  27217  fsumdvdsmul  27324  dchrmullid  27381  bcp1ctr  27408  lgsneg  27450  lgsneg1  27451  lgsdir2  27459  lgsdir  27461  lgsdi  27463  lgsquad2lem2  27514  pntleml  27740  lrold  28055  abssnid  28401  om2noseqfo  28456  n0seo  28579  pw2cutp1  28619  motgrp  28777  lmiisolem  29062  egrsubgr  29567  iswwlksnon  30142  iswspthsnon  30145  bafval  30896  ipidsq  31002  ipasslem1  31123  pjclem2  32488  cvmdi  32616  imadifxp  32886  2ndimaxp  32931  suppun2  32969  iundisjcnt  33083  dpfrac1  33151  gsumpart  33323  suppgsumssiun  33332  cycpmco2rn  33385  cyc3genpmlem  33411  fracbas  33568  resvsca  33594  psrgsum  33882  psrmonmul  33884  psrmonprod  33886  rspectset  34200  bayesth  34773  ofcccat  34877  subfacp1lem6  35575  satfdm  35759  mvtval  35890  mexval  35892  mexval2  35893  mdvval  35894  mrsubfval  35898  mrsubvrs  35912  msubfval  35914  elmsubrn  35918  mvhfval  35923  mpstval  35925  msrfval  35927  mstaval  35934  mthmval  35965  bccolsum  36129  dfrdg2  36183  dfrdg3  36184  dfrdg4  36341  ordtoplem  36834  ordcmp  36846  curunc  38140  matunitlindflem2  38155  poimirlem6  38164  poimirlem7  38165  poimirlem11  38169  poimirlem12  38170  poimirlem13  38171  poimirlem14  38172  poimirlem16  38174  poimirlem19  38177  poimirlem21  38179  poimirlem22  38180  poimirlem27  38185  poimirlem31  38189  poimirlem32  38190  itg2addnclem2  38210  ibladdnclem  38214  iblabsnclem  38221  iblabsnc  38222  iblmulc2nc  38223  ftc1anclem8  38238  pmodN  40513  tgrpgrplem  41412  tendoplass  41446  tendoicl  41459  erngdvlem3  41653  dvhvaddass  41760  dib0  41827  dib1dim2  41831  diclspsn  41857  cdlemn8  41867  dihopelvalcpre  41911  djhcom  42068  evlsbagval  43209  kelac2  43683  mendbas  43798  mendring  43806  iscard4  44150  relexp01min  44330  relexpaddss  44335  iotain  45018  addrcom  45074  rnsnf  45793  limsupvaluz  46313  itgsinexplem1  46559  volioc  46577  dirkertrigeqlem1  46703  fourierdlem104  46815  sqwvfoura  46833  sqwvfourb  46834  hoicvr  47153  fzopredsuc  47949  ppivalnn  48272  fppr2odd  48384  dfnbgr5  48504  gpgprismgr4cycllem10  48757  rngccatidALTV  48925  ringccatidALTV  48959  0dig2pr01  49274  nn0sumshdiglemB  49284  imaidfu2  49773  oppczeroo  49899  dfswapf2  49923  oppc1stf  49950  oppc2ndf  49951  prcof1  50050  setc1onsubc  50264  termolmd  50332