Theorem 3eqtr4a 2802

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

Syntax hints:   → wi 4   = wceq 1539

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728

This theorem is referenced by:  rabsnif  4663  uniintsn  4925  iinvdif  5016  iununi  5035  dmxpid  5851  rnxpid  6091  csbrn  6121  dmsnsnsn  6138  opswap  6147  xpcoid  6208  predres  6257  unizlim  6402  fvco4i  6901  fndmdifcom  6952  fmptsng  7072  fmptsnd  7073  csbov  7350  ordunisuc  7711  offres  7858  1stval2  7880  2ndval2  7881  cnvf1olem  7982  fparlem3  7986  fparlem4  7987  frrlem12  8144  seqomlem1  8312  ecovcom  8643  ecovass  8644  ecovdi  8645  resixpfo  8755  mapunen  8971  cardidm  9761  cardiun  9784  alephcard  9872  cardalephex  9892  cardcf  10054  cfidm  10077  alephsing  10078  itunisuc  10221  itunitc  10223  ituniiun  10224  alephadd  10379  alephreg  10384  pwcfsdom  10385  addcompq  10752  addcomnq  10753  mulcompq  10754  mulcomnq  10755  addassnq  10760  mulassnq  10761  addid1  11201  zeo  12452  xnegneg  12994  xaddcom  13020  xaddid1  13021  xnegdi  13028  xmulid1  13059  xadddilem  13074  ixxin  13142  fzsuc2  13360  expneg  13836  sq01  13986  facp1  14038  bcpasc  14081  hashfzp1  14191  resunimafz0  14202  hashf1lem1  14213  hashf1lem1OLD  14214  hashf1  14216  ccat1st1st  14380  swrdccatin1  14483  swrdccat3blem  14497  repswsymballbi  14538  cshwmodn  14553  cshwlen  14557  repswcshw  14570  trclun  14770  relexpcnv  14791  relexpaddd  14810  absexp  15061  sqreulem  15116  fsumf1o  15480  fsumadd  15497  fsumrev2  15539  fsumparts  15563  fsumrelem  15564  fprodf1o  15701  fprodmul  15715  fproddiv  15716  fprodfac  15728  fallfacfwd  15791  efexp  15855  tanval2  15887  sadeq  16224  smumullem  16244  smumul  16245  gcdcom  16265  gcd0id  16271  gcdass  16300  lcmcom  16343  lcmneg  16353  lcmass  16364  nn0gcdsq  16501  dfphi2  16520  pcneg  16620  setscom  16926  strfvi  16936  fveqprc  16937  oveqprc  16938  setsnidOLD  16956  ressbas  16992  ressbasOLD  16993  ressinbas  17000  ressress  17003  firest  17188  topnval  17190  xpsfeq  17319  xpsaddlem  17329  xpsvsca  17333  oppchomfval  17468  oppchomfvalOLD  17469  oppcbasOLD  17474  rescbas  17586  rescbasOLD  17587  rescco  17590  resccoOLD  17591  cofuass  17649  fucbas  17722  fuchom  17723  fuchomOLD  17724  setccatid  17844  estrccatid  17893  xpcbas  17940  oduleval  18052  odulub  18170  oduglb  18172  ipotset  18296  efmndbas  18555  efmndbasabf  18556  symggrplem  18568  smndex1mndlem  18593  pwmnd  18621  grpinvfvi  18667  cntrval  18970  cntzval  18972  oppgplusfval  18997  snsymgefmndeq  19047  symgvalstruct  19049  symgvalstructOLD  19050  pmtrprfval  19140  m1expaddsub  19151  sylow1lem2  19249  sylow3lem1  19277  oppglsm  19292  gsumzsplit  19573  gsum2dlem2  19617  gsumcom2  19621  dprd2dlem2  19688  dprd2da  19690  dmdprdsplit2lem  19693  mgpplusg  19769  mgpress  19780  mgpressOLD  19781  ringidval  19784  opprmulfval  19909  abvtrivd  20145  sralem  20484  sralemOLD  20485  srasca  20492  srascaOLD  20493  sravsca  20494  sravscaOLD  20495  sraip  20496  rlmval  20506  zlmlemOLD  20764  zlmsca  20771  zlmvsca  20772  psgninv  20832  ocvval  20917  thlbas  20946  thlbasOLD  20947  thlle  20948  thlleOLD  20949  thloc  20951  dsmmval2  20988  psrmulr  21198  mplmonmul  21282  mplcoe3  21284  opsrbaslem  21295  opsrbaslemOLD  21296  opsrtoslem2  21308  psr1val  21402  ply1basfvi  21457  ply1plusgfvi  21458  psr1sca2  21467  evl1fval1lem  21541  mattpos1  21650  mdettpos  21805  smadiadetglem1  21865  tgdif0  22187  indislem  22195  restco  22360  txtopon  22787  txindislem  22829  qtopres  22894  hmphindis  22993  ptuncnv  23003  snclseqg  23312  tsmssplit  23348  ussval  23456  tuslem  23463  tuslemOLD  23464  setsmsbas  23673  setsmsbasOLD  23674  tnglemOLD  23842  tngds  23856  tngdsOLD  23857  tngtset  23858  pcoass  24232  cphsqrtcl2  24395  rrxcph  24601  ovolunlem1a  24705  ioorinv  24785  itg11  24900  itg1mulc  24914  itg2cnlem1  24971  iblss2  25015  ibladdlem  25029  itgfsum  25036  iblabslem  25037  iblabs  25038  ditgneg  25066  deg1fvi  25295  dgrco  25481  logfac  25801  cxpexp  25868  cxpmul2  25889  cxpsqrt  25903  cxpsqrtth  25929  dvcxp1  25938  dvcxp2  25939  ang180lem1  26004  mcubic  26042  quart1  26051  reasinsin  26091  atanlogaddlem  26108  atantayl2  26133  log2tlbnd  26140  basellem2  26276  basellem3  26277  basellem5  26279  basellem8  26282  dchrmulid2  26445  bcp1ctr  26472  lgsneg  26514  lgsneg1  26515  lgsdir2  26523  lgsdir  26525  lgsdi  26527  lgsquad2lem2  26578  pntleml  26804  motgrp  26949  lmiisolem  27202  ttglemOLD  27284  egrsubgr  27689  iswwlksnon  28263  iswspthsnon  28266  bafval  29011  ipidsq  29117  ipasslem1  29238  pjclem2  30603  cvmdi  30731  imadifxp  30985  2ndimaxp  31029  iundisjcnt  31164  dpfrac1  31211  gsumpart  31360  cycpmco2rn  31437  cyc3genpmlem  31463  resvsca  31574  rspectset  31861  indval2  32027  bayesth  32451  ofcccat  32567  plymulx  32572  subfacp1lem6  33192  satfdm  33376  mvtval  33507  mexval  33509  mexval2  33510  mdvval  33511  mrsubfval  33515  mrsubvrs  33529  msubfval  33531  elmsubrn  33535  mvhfval  33540  mpstval  33542  msrfval  33544  mstaval  33551  mthmval  33582  bccolsum  33750  dfrdg2  33816  dfrdg3  33817  lrold  34122  dfrdg4  34298  ordtoplem  34669  ordcmp  34681  curunc  35803  matunitlindflem2  35818  poimirlem6  35827  poimirlem7  35828  poimirlem11  35832  poimirlem12  35833  poimirlem13  35834  poimirlem14  35835  poimirlem16  35837  poimirlem19  35840  poimirlem21  35842  poimirlem22  35843  poimirlem27  35848  poimirlem31  35852  poimirlem32  35853  itg2addnclem2  35873  ibladdnclem  35877  iblabsnclem  35884  iblabsnc  35885  iblmulc2nc  35886  ftc1anclem8  35901  pmodN  37906  tgrpgrplem  38805  tendoplass  38839  tendoicl  38852  erngdvlem3  39046  dvhvaddass  39153  dib0  39220  dib1dim2  39224  diclspsn  39250  cdlemn8  39260  dihopelvalcpre  39304  djhcom  39461  nn0expgcd  40372  kelac2  40928  mendbas  41047  mendring  41055  iscard4  41178  relexp01min  41359  relexpaddss  41364  iotain  42073  addrcom  42131  rnsnf  42765  itgsinexplem1  43544  volioc  43562  dirkertrigeqlem1  43688  fourierdlem104  43800  sqwvfoura  43818  sqwvfourb  43819  fzopredsuc  44873  fppr2odd  45241  rngccatidALTV  45605  ringccatidALTV  45668  0dig2pr01  46014  nn0sumshdiglemB  46024