Theorem 3eqtr4i 2796

Description: An inference from three chained equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr4i.1	⊢ 𝐴 = 𝐵
3eqtr4i.2	⊢ 𝐶 = 𝐴
3eqtr4i.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3eqtr4i	⊢ 𝐶 = 𝐷

Proof of Theorem 3eqtr4i

Step	Hyp	Ref	Expression
1		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
2		3eqtr4i.3	. . 3 ⊢ 𝐷 = 𝐵
3		3eqtr4i.1	. . 3 ⊢ 𝐴 = 𝐵
4	2, 3	eqtr4i 2789	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2789	1 ⊢ 𝐶 = 𝐷

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  cbvrabv  3426  cbvrabw  3450  cbvrab  3453  cbvcsbw  3861  cbvcsb  3862  cbvcsbv  3863  csbcow  3866  csbco  3867  cbvrabcsfw  3892  cbvrabcsf  3896  incom  4109  in13  4130  in31  4131  in4  4133  un4  4176  symdifcom  4202  indifcom  4231  indir  4234  undir  4235  indifdir  4243  difdif2  4244  notrab  4270  dfnul3  4285  dfif5  4502  rabsnifsb  4685  prcom  4695  tprot  4712  tpcoma  4713  tpcomb  4714  tpass  4715  qdassr  4717  pwsn  4832  pw0  4835  pwpw0  4836  cbviun  4998  cbviin  4999  cbviung  5000  cbviing  5001  cbviunv  5002  cbviinv  5003  iunrab  5016  iunin1  5035  iinuni  5063  cbvopab  5183  cbvopabv  5184  cbvopab1  5185  cbvopab1g  5186  cbvopab2  5187  cbvopab1s  5188  cbvopab1v  5189  cbvopab2v  5190  unopab  5191  cbvmptf  5211  cbvmptfg  5212  cbvmptv  5215  iunopab  5541  dfid4  5554  dfid2  5555  dfid3  5556  rabxp  5706  fconstmpt  5720  csbxp  5760  cnvi  5875  cnvco  5879  csbdm  5891  rnmpt  5951  csbres  5989  resundi  6000  resundir  6001  resindi  6002  resindir  6003  rescom  6009  resima  6074  imadmrnOLD  6086  cnvimarndmOLD  6099  cnvin  6153  rnun  6154  imaundi  6159  cnvxpOLD  6166  imainrect  6191  csbrn  6223  imacnvcnv  6226  resdmres  6252  imadmres  6254  resdifdir  6257  mptpreima  6258  dfpred3  6341  predin  6356  predun  6357  preddif  6358  frpoind  6371  cbviotaw  6527  cbviotavw  6528  cbviota  6529  sb8iota  6531  resdif  6876  opabiotadm  6997  fndmin  7075  fninfp  7210  cbvriotaw  7417  cbvriotavw  7418  cbvriota  7421  riotarab  7450  dfoprab2  7509  cbvoprab1  7538  cbvoprab2  7539  cbvoprab12  7540  cbvoprab12v  7541  cbvoprab3  7542  cbvoprab3v  7543  cbvmpox  7544  cbvmpov  7546  resoprab  7569  caov32  7680  caov31  7682  caov4  7684  caovlem2  7689  mpt3mpt  7717  uniuni  7808  zfrep6OLD  8001  ofmres  8030  dfopab2  8098  dfxp3  8107  dmmpossx  8112  fmpox  8113  fsplit  8165  ovtpos  8296  tposco  8312  frrlem5  8346  tfrlem10  8433  o2p2e4  8587  0map0sn0  8951  mapsncnv  8959  cbvixp  8980  cbvixpv  8981  xpcomco  9124  sbthlem6  9149  ttrclresv  9755  frind  9791  cardf2  10061  alephcard  10188  alephfplem1  10222  xp2dju  10294  djuassen  10296  infdju1  10307  pwdju1  10308  ackbij1lem14  10349  compsscnv  10488  dffin1-5  10505  ituniiun  10539  axdc2lem  10565  axdc3lem4  10570  axcclem  10574  pwcfsdom  10707  dmaddpi  11014  dmmulpi  11015  adderpqlem  11078  addassnq  11082  mulcanenq  11084  addcmpblnr  11193  mulcmpblnrlem  11194  ltsrpr  11201  mulgt0sr  11229  sqgt0sr  11230  axi2m1  11283  negiso  12337  nummac  12904  decsubi  12922  9t11e99OLD  12990  fztpval  13760  seqval  14195  sqrecii  14366  sqdivi  14368  binom2i  14397  4bc2eq6  14514  hashgval  14518  revs1  14956  cats1cat  15054  trclublem  15191  shftdm  15267  shftidt2  15277  cji  15369  cbvsum  15906  cbvsumv  15907  sumfc  15919  ackbijnn  16041  cbvprod  16126  cbvprodv  16127  prodeq1i  16129  prodfc  16156  fsumcube  16270  divalglem2  16609  nn0expgcd  16782  nn0gcdsq  16972  prmrec  17144  hashbc0  17227  dec5nprm  17288  dec2nprm  17289  gcdi  17295  decsplit  17304  1259lem1  17353  1259lem4  17356  4001lem1  17363  phlstr  17563  oduval  18512  oduleval  18513  odubas  18515  lubdm  18573  glbdm  18586  degenmgmopdm  19184  degenmgm2opdm  19188  oppgid  19621  symgbas0  19654  gsumcom2  20240  ringidval  20460  oppr1  20631  dfrhm2  20755  rmodislmod  21256  cnfldsub  21758  cnflddiv  21760  dvdsrzring  21822  pjdm  22068  pjfval2  22070  opsrtoslem1  22419  restco  23537  ufprim  24283  tgioo3  25180  oprpiece1res1  25327  oprpiece1res2  25328  volfiniun  25923  vitalilem4  25987  cbvitg  26151  cbvitgv  26152  itgresr  26154  cbvditg  26229  plyid  26582  coeidp  26637  dgrid  26638  sincos3rdpi  26902  logblog  27177  ang180lem2  27195  1cubrlem  27226  asin1  27279  log2ublem2  27332  log2ublem3  27333  emcllem5  27384  lgsdir2lem5  27713  lgsquadlem3  27766  2lgslem1b  27776  2lgsoddprmlem3d  27797  noextend  28080  nosupbday  28119  nosupbnd1  28128  nosupbnd2  28130  noinfbday  28134  noinfbnd1  28143  dmcuts  28234  madeval2  28276  neg0s  28469  neg1s  28470  cchhllem  29521  ax5seglem7  29570  vtxval0  29674  iedgval0  29675  finsumvtxdg2ssteplem1  30183  wwlksnfi  30552  1wlkdlem1  30785  ex-un  31082  ex-pw  31087  ex-cnv  31095  ex-co  31096  bafval  31263  vsfval  31292  cnnvba  31338  cnnvm  31341  ip2dii  31503  siilem1  31510  h2hcau  31638  hvsubsub4i  31718  hvnegdii  31721  normlem3  31771  normlem8  31776  norm-iii-i  31798  normpar2i  31815  polid2i  31816  chjassi  32145  chj4i  32182  h1de2i  32212  spanunsni  32238  fh3i  32282  fh4i  32283  qlax4i  32289  qlaxr3i  32295  3oalem5  32325  pjadjii  32333  pjsubii  32337  hoadd32i  32437  cnvadj  32551  hh0oi  32562  hhcno  32563  hhcnf  32564  nmopnegi  32624  lnophmlem2  32676  branmfn  32764  dmrab  33192  3unrab  33198  abrexexd  33204  cbviunf  33248  maprnin  33419  dpmul10  33557  dpexpp1  33570  dpadd3  33574  dpmul  33575  dpmul4  33576  psgnfzto1st  33765  cycpmconjs  33816  fracbas  33971  cos9thpiminplylem5  34529  lmlimxrge0  34691  zrhre  34762  qqhre  34763  rrhre  34764  cbvesum  34785  cbvesumv  34786  unibrsiga  34930  eulerpartlemt  35114  eulerpartgbij  35115  ballotlemrinv  35277  hgt750lem2  35392  bnj1146  35532  bnj893  35669  bnj1234  35754  r11  35850  r12  35851  dfk12  36053  dfk22  36054  dfk32  36055  subfacp1lem1  36152  kur14lem2  36180  kur14lem5  36183  kur14lem7  36185  cvmscld  36246  satfv1lem  36335  fmla0  36355  mvtval  36473  mthmpps  36555  fixun  36886  rabeqbii  37198  iuneq12i  37199  iineq1i  37200  iineq12i  37201  riotaeqbii  37202  ixpeq1i  37204  sumeq2si  37206  prodeq2si  37208  itgeq12i  37210  ditgeq123i  37213  cbvcsbvw2  37235  cbviunvw2  37236  cbviinvw2  37237  cbvmptvw2  37238  cbvriotavw2  37240  cbvoprab1vw  37241  cbvoprab2vw  37242  cbvoprab123vw  37243  cbvoprab23vw  37244  cbvoprab13vw  37245  cbvmpovw2  37246  cbvmpo1vw2  37247  cbvmpo2vw2  37248  cbvixpvw2  37249  cbvprodvw2  37251  cbvitgvw2  37252  cbvditgvw2  37253  ttcun  37515  ttciun  37517  bj-inrab  38055  bj-inrab3  38057  bj-gabeqis  38066  bj-pr1un  38131  bj-pr2un  38145  coi1res  38199  coi2res  38200  coresrn  38204  bj-dfid2ALT  38250  bj-mpomptALT  38311  rnmptsn  38526  f1omptsnlem  38527  rabiun  38789  phpreu  38795  poimirlem18  38824  ovoliunnfl  38848  voliunnfl  38850  mbfposadd  38853  asindmre  38889  abeqin  39452  rncnvepres  39507  qsresid  39529  dmxrn  39585  rnxrn  39619  xrnres  39623  xrnres2  39624  xrnres3  39625  dmxrncnvepres2  39631  dfsucmap3  39661  dfsucmap2  39662  rncossdmcoss  39743  1cosscnvxrn  39763  refrelsredund4  39914  mpets  40154  dfpetparts2  40170  dfpeters2  40172  petseq  40174  pets2eq  40175  cdleme25cv  41681  sn-iotalemcor  43543  sqdeccom12  43612  sumcubes  43636  resuppsinopn  43680  sn-00idlem2  43716  sn-1ticom  43752  mendsca  44448  areaquad  44479  onsucrn  44534  df3o2  44576  df3o3  44577  omcl3g  44597  dfno2  44690  cnvrcl0  44886  sqrtcvallem1  44892  trclrelexplem  44972  k0004val0  45415  iuneq1i  46374  cbvmpo2  46385  cbvmpo1  46386  cbvrabv2w  46416  mptssid  46526  fprodabs2  46880  stoweidlem13  47296  wallispilem4  47351  fourierdlem94  47483  fourierdlem102  47491  fourierdlem111  47500  fourierdlem112  47501  fourierdlem113  47502  fourierdlem114  47503  41prothprmlem2  48976  2exp340mod341  49104  8exp8mod9  49107  nfermltl8rev  49113  stgr1  49332  gpgprismgr4cycllem6  49471  gpgprismgr4cycllem9  49474  gpgprismgr4cycllem10  49475  bru4  49752  bru3eq  49756  cbvmpox2  49779  dmmpossx2  49780  zlmodzxzequa  49939  zlmodzxzequap  49942  2sphere  50192  resinsn  50316  dfswapf2  50714