Theorem 3eqtr4i 2642

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 2635	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2635	1 ⊢ 𝐶 = 𝐷

Syntax hints:   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  rabswap  3098  rabbiia  3161  cbvrab  3171  cbvcsb  3504  csbco  3509  cbvrabcsf  3534  un4  3735  in13  3788  in31  3789  in4  3791  symdifcom  3807  indifcom  3831  indir  3834  undir  3835  difdif2  3843  notrab  3863  dfnul3  3877  rab0OLD  3910  dfif5  4052  rabsnifsb  4201  prcom  4211  tprot  4228  tpcoma  4229  tpcomb  4230  tpass  4231  qdassr  4233  pw0  4283  pwpw0  4284  pwsn  4366  pwsnALT  4367  int0OLD  4426  rabasiun  4459  cbviun  4493  cbviin  4494  iunrab  4503  iunin1  4521  iinuni  4545  cbvopab  4653  cbvopab1  4655  cbvopab2  4656  cbvopab1s  4657  cbvopab2v  4659  unopab  4660  cbvmptf  4676  cbvmpt  4677  iunopab  4936  dfid3  4954  dfid4  4955  rabxp  5078  fconstmpt  5085  csbxp  5123  inxp  5176  cnvco  5230  csbdm  5240  rnmpt  5292  csbres  5320  resundi  5330  resundir  5331  resindi  5332  resindir  5333  rescom  5343  resima  5351  imadmrn  5395  cnvimarndm  5405  cnvi  5456  cnvin  5459  rnun  5460  imaundi  5464  cnvxp  5470  imainrect  5494  csbrn  5514  imacnvcnv  5517  resdmres  5543  imadmres  5544  mptpreima  5545  dfpred3  5607  predin  5620  predun  5621  preddif  5622  wfi  5630  cbviota  5773  sb8iota  5775  resdif  6070  opabiotadm  6170  fndmin  6232  fninfp  6345  cbvriota  6521  dfoprab2  6599  cbvoprab1  6625  cbvoprab2  6626  cbvoprab12  6627  cbvoprab3  6629  cbvmpt2x  6631  resoprab  6654  caov32  6759  caov31  6761  caov4  6763  caovlem2  6768  uniuni  6865  zfrep6  7027  ofmres  7055  dfopab2  7113  dfxp3  7119  dmmpt2ssx  7124  fmpt2x  7125  fsplit  7169  ovtpos  7254  tposco  7270  tfrlem10  7370  o2p2e4  7508  mapsncnv  7790  cbvixp  7811  xpcomco  7935  sbthlem6  7960  1sdom  8048  cardf2  8652  alephcard  8776  alephfplem1  8810  pwcda1  8899  ackbij1lem14  8938  compsscnv  9076  dffin1-5  9093  ituniiun  9127  axdc2lem  9153  axdc3lem4  9158  axcclem  9162  pwcfsdom  9284  dmaddpi  9591  dmmulpi  9592  adderpqlem  9655  addassnq  9659  mulcanenq  9661  addcmpblnr  9769  mulcmpblnrlem  9770  ltsrpr  9777  mulgt0sr  9805  sqgt0sr  9806  axi2m1  9859  negiso  10880  nummac  11434  decsubi  11459  decsubiOLD  11460  9t11e99  11547  9t11e99OLD  11548  fzprval  12271  fztpval  12272  seqval  12674  sqrecii  12808  sqdivi  12810  binom2i  12836  4bc2eq6  12978  hashgval  12982  revs1  13365  cats1cat  13457  trclublem  13582  shftdm  13659  shftidt2  13669  cji  13747  cbvsum  14273  sumfc  14287  ackbijnn  14399  cbvprod  14484  prodfc  14514  fsumcube  14630  divalglem2  14956  nn0gcdsq  15298  prmreclem2  15459  prmrec  15464  hashbc0  15547  dec5nprm  15608  dec2nprm  15609  gcdi  15615  decexp2  15617  decsplit  15625  decsplitOLD  15629  1259lem1  15676  1259lem4  15679  4001lem1  15686  dfpleOLD  15789  strlemor2  15797  strlemor3  15798  phlstr  15857  lubdm  16802  glbdm  16815  oduval  16953  oduleval  16954  odubas  16956  oppgid  17609  symgbas0  17637  gsumcom2  18197  ringidval  18326  oppr1  18457  dfrhm2  18540  opsrtoslem1  19305  cnfldsub  19593  cnflddiv  19595  dvdsrzring  19650  pjdm  19870  pjfval2  19872  restco  20778  cnmptid  21274  ufprim  21523  tgioo3  22416  oprpiece1res1  22558  oprpiece1res2  22559  volfiniun  23122  vitalilem4  23186  cbvitg  23348  itgresr  23351  iblcnlem1  23360  cbvditg  23424  sincos3rdpi  24072  logblog  24330  ang180lem2  24340  1cubrlem  24368  asin1  24421  log2ublem2  24474  log2ublem3  24475  emcllem5  24526  lgsdir2lem5  24854  lgsquadlem3  24907  2lgslem1b  24917  2lgsoddprmlem3d  24938  cchhllem  25567  ax5seglem7  25615  axlowdimlem4  25625  vtxval0  25714  iedgval0  25715  usgraop  25879  usgrafilem1  25940  cusgrasizeindslem1  26002  vdgrun  26428  vdgrfiun  26429  vdegp1bi  26512  konigsberg  26514  ex-un  26673  ex-pw  26678  ex-cnv  26686  ex-co  26687  bafval  26843  vsfval  26872  cnnvba  26918  cnnvm  26921  ip2dii  27083  siilem1  27090  h2hcau  27220  hvsubsub4i  27300  hvnegdii  27303  normlem3  27353  normlem8  27358  norm-iii-i  27380  normpar2i  27397  polid2i  27398  chjassi  27729  chj4i  27766  h1de2i  27796  spanunsni  27822  fh3i  27866  fh4i  27867  qlax4i  27873  qlaxr3i  27879  3oalem5  27909  pjadjii  27917  pjsubii  27921  hoadd32i  28021  cnvadj  28135  hh0oi  28146  hhcno  28147  hhcnf  28148  nmopnegi  28208  lnophmlem2  28260  branmfn  28348  rabrab  28722  abrexexd  28731  cbviunf  28755  maprnin  28894  psgnfzto1st  29186  lmlimxrge0  29322  rrhre  29393  cbvesum  29431  unibrsiga  29576  eulerpartlemt  29760  eulerpartgbij  29761  ballotlem2  29877  ballotlemrinv  29922  bnj1146  30116  bnj893  30252  bnj1234  30335  subfacp1lem1  30415  kur14lem2  30443  kur14lem5  30446  kur14lem7  30448  cvmscld  30509  mvtval  30651  mthmpps  30733  frind  30984  fixun  31186  bj-inrab  32115  bj-pr1un  32184  bj-pr2un  32198  bj-mpt2mptALT  32253  f1omptsnlem  32359  rabiun  32552  phpreu  32563  poimirlem18  32597  ovoliunnfl  32621  voliunnfl  32623  mbfposadd  32627  asindmre  32665  cdleme25cv  34664  mendsca  36778  areaquad  36821  cnvrcl0  36951  trclrelexplem  37022  df3o2  37342  df3o3  37343  cbvmpt22  38305  cbvmpt21  38306  fprodabs2  38662  stoweidlem13  38906  wallispilem4  38961  fourierdlem94  39093  fourierdlem102  39101  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  fourierdlem114  39113  41prothprmlem2  40073  11wlkdlem1  41304  cbvmpt2x2  41907  dmmpt2ssx2  41908  zlmodzxzequa  42079  zlmodzxzequap  42082