Theorem 3eqtr4a 2803

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 2793	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2780	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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  rabsnif  4723  uniintsn  4985  iinvdif  5080  iununi  5099  dmxpid  5941  rnxpid  6193  csbrn  6223  dmsnsnsn  6240  opswap  6249  xpcoid  6310  predres  6360  unizlim  6507  fvco4i  7010  fndmdifcom  7063  fmptsng  7188  fmptsnd  7189  csbov  7476  ordunisuc  7852  offres  8008  1stval2  8031  2ndval2  8032  cnvf1olem  8135  fparlem3  8139  fparlem4  8140  frrlem12  8322  seqomlem1  8490  ecovcom  8863  ecovass  8864  ecovdi  8865  resixpfo  8976  mapunen  9186  cardidm  9999  cardiun  10022  alephcard  10110  cardalephex  10130  cardcf  10292  cfidm  10315  alephsing  10316  itunisuc  10459  itunitc  10461  ituniiun  10462  alephadd  10617  alephreg  10622  pwcfsdom  10623  addcompq  10990  addcomnq  10991  mulcompq  10992  mulcomnq  10993  addassnq  10998  mulassnq  10999  addrid  11441  zeo  12704  xnegneg  13256  xaddcom  13282  xaddrid  13283  xnegdi  13290  xmulrid  13321  xadddilem  13336  ixxin  13404  fzsuc2  13622  expneg  14110  sq01  14264  facp1  14317  bcpasc  14360  hashfzp1  14470  resunimafz0  14484  hashf1lem1  14494  hashf1  14496  ccat1st1st  14666  swrdccatin1  14763  swrdccat3blem  14777  repswsymballbi  14818  cshwmodn  14833  cshwlen  14837  repswcshw  14850  trclun  15053  relexpcnv  15074  relexpaddd  15093  absexp  15343  sqreulem  15398  fsumf1o  15759  fsumadd  15776  fsumrev2  15818  fsumparts  15842  fsumrelem  15843  fprodf1o  15982  fprodmul  15996  fproddiv  15997  fprodfac  16009  fallfacfwd  16072  efexp  16137  tanval2  16169  sadeq  16509  smumullem  16529  smumul  16530  gcdcom  16550  gcd0id  16556  gcdass  16584  nn0expgcd  16601  lcmcom  16630  lcmneg  16640  lcmass  16651  nn0gcdsq  16789  dfphi2  16811  pcneg  16912  setscom  17217  strfvi  17227  fveqprc  17228  oveqprc  17229  setsnidOLD  17246  ressbas  17280  ressbasOLD  17281  ressinbas  17291  ressress  17293  firest  17477  topnval  17479  xpsfeq  17608  xpsaddlem  17618  xpsvsca  17622  oppchomfval  17757  rescbas  17873  rescco  17876  cofuass  17934  fucbas  18008  fuchom  18009  setccatid  18129  estrccatid  18176  xpcbas  18223  oduleval  18334  odulub  18452  oduglb  18454  ipotset  18578  efmndbas  18884  efmndbasabf  18885  symggrplem  18897  smndex1mndlem  18922  pwmnd  18950  grpinvfvi  19000  cntrval  19337  cntzval  19339  oppgplusfval  19366  snsymgefmndeq  19412  symgvalstruct  19414  symgvalstructOLD  19415  pmtrprfval  19505  m1expaddsub  19516  sylow1lem2  19617  sylow3lem1  19645  oppglsm  19660  gsumzsplit  19945  gsum2dlem2  19989  gsumcom2  19993  dprd2dlem2  20060  dprd2da  20062  dmdprdsplit2lem  20065  mgpplusg  20141  mgpress  20147  ringidval  20180  opprmulfval  20336  abvtrivd  20833  sralem  21175  sralemOLD  21176  srasca  21183  srascaOLD  21184  sravsca  21185  sravscaOLD  21186  sraip  21187  rlmval  21198  zlmlemOLD  21528  zlmsca  21535  zlmvsca  21536  psgninv  21600  ocvval  21685  thlbas  21714  thlbasOLD  21715  thlle  21716  thlleOLD  21717  thloc  21719  dsmmval2  21756  psrmulr  21962  mplmonmul  22054  mplcoe3  22056  opsrbaslem  22067  opsrbaslemOLD  22068  opsrtoslem2  22080  psr1val  22187  ply1basfvi  22242  ply1plusgfvi  22243  psr1sca2  22252  evl1fval1lem  22334  mattpos1  22462  mdettpos  22617  smadiadetglem1  22677  tgdif0  22999  indislem  23007  restco  23172  txtopon  23599  txindislem  23641  qtopres  23706  hmphindis  23805  ptuncnv  23815  snclseqg  24124  tsmssplit  24160  ussval  24268  tuslem  24275  tuslemOLD  24276  setsmsbas  24485  setsmsbasOLD  24486  tnglemOLD  24654  tngds  24668  tngdsOLD  24669  tngtset  24670  pcoass  25057  cphsqrtcl2  25220  rrxcph  25426  ovolunlem1a  25531  ioorinv  25611  itg11  25726  itg1mulc  25739  itg2cnlem1  25796  iblss2  25841  ibladdlem  25855  itgfsum  25862  iblabslem  25863  iblabs  25864  ditgneg  25892  deg1fvi  26124  dgrco  26315  logfac  26643  cxpexp  26710  cxpmul2  26731  cxpsqrt  26745  cxpsqrtth  26772  dvcxp1  26782  dvcxp2  26783  ang180lem1  26852  mcubic  26890  quart1  26899  reasinsin  26939  atanlogaddlem  26956  atantayl2  26981  log2tlbnd  26988  basellem2  27125  basellem3  27126  basellem5  27128  basellem8  27131  fsumdvdsmul  27238  dchrmullid  27296  bcp1ctr  27323  lgsneg  27365  lgsneg1  27366  lgsdir2  27374  lgsdir  27376  lgsdi  27378  lgsquad2lem2  27429  pntleml  27655  lrold  27935  abssnid  28267  om2noseqfo  28304  n0seo  28405  zs12bday  28424  motgrp  28551  lmiisolem  28804  ttglemOLD  28886  egrsubgr  29294  iswwlksnon  29873  iswspthsnon  29876  bafval  30623  ipidsq  30729  ipasslem1  30850  pjclem2  32215  cvmdi  32343  imadifxp  32614  2ndimaxp  32656  suppun2  32693  iundisjcnt  32800  indval2  32839  dpfrac1  32874  gsumpart  33060  cycpmco2rn  33145  cyc3genpmlem  33171  fracbas  33307  resvsca  33356  rspectset  33865  bayesth  34441  ofcccat  34558  plymulx  34563  subfacp1lem6  35190  satfdm  35374  mvtval  35505  mexval  35507  mexval2  35508  mdvval  35509  mrsubfval  35513  mrsubvrs  35527  msubfval  35529  elmsubrn  35533  mvhfval  35538  mpstval  35540  msrfval  35542  mstaval  35549  mthmval  35580  bccolsum  35739  dfrdg2  35796  dfrdg3  35797  dfrdg4  35952  ordtoplem  36436  ordcmp  36448  curunc  37609  matunitlindflem2  37624  poimirlem6  37633  poimirlem7  37634  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem14  37641  poimirlem16  37643  poimirlem19  37646  poimirlem21  37648  poimirlem22  37649  poimirlem27  37654  poimirlem31  37658  poimirlem32  37659  itg2addnclem2  37679  ibladdnclem  37683  iblabsnclem  37690  iblabsnc  37691  iblmulc2nc  37692  ftc1anclem8  37707  pmodN  39852  tgrpgrplem  40751  tendoplass  40785  tendoicl  40798  erngdvlem3  40992  dvhvaddass  41099  dib0  41166  dib1dim2  41170  diclspsn  41196  cdlemn8  41206  dihopelvalcpre  41250  djhcom  41407  evlsbagval  42576  kelac2  43077  mendbas  43192  mendring  43200  iscard4  43546  relexp01min  43726  relexpaddss  43731  iotain  44436  addrcom  44494  rnsnf  45189  itgsinexplem1  45969  volioc  45987  dirkertrigeqlem1  46113  fourierdlem104  46225  sqwvfoura  46243  sqwvfourb  46244  fzopredsuc  47335  fppr2odd  47718  dfnbgr5  47837  rngccatidALTV  48188  ringccatidALTV  48222  0dig2pr01  48531  nn0sumshdiglemB  48541  dfswapf2  48967