Theorem 3eqtr4i 2794

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 2787	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2787	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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  cbvrabv  3423  cbvrabw  3447  cbvrab  3450  cbvcsbw  3857  cbvcsb  3858  cbvcsbv  3859  csbcow  3862  csbco  3863  cbvrabcsfw  3888  cbvrabcsf  3892  un4  4121  incom  4155  in13  4176  in31  4177  in4  4179  symdifcom  4200  indifcom  4229  indir  4232  undir  4233  indifdir  4241  difdif2  4242  notrab  4268  dfnul3  4283  dfif5  4499  rabsnifsb  4683  prcom  4693  tprot  4710  tpcoma  4711  tpcomb  4712  tpass  4713  qdassr  4715  pw0  4773  pwpw0  4774  pwsn  4860  cbviun  4993  cbviin  4994  cbviung  4995  cbviing  4996  cbviunv  4997  cbviinv  4998  iunrab  5011  iunin1  5030  iinuni  5058  cbvopab  5177  cbvopabv  5178  cbvopab1  5179  cbvopab1g  5180  cbvopab2  5181  cbvopab1s  5182  cbvopab1v  5183  cbvopab2v  5184  unopab  5185  cbvmptf  5205  cbvmptfg  5206  cbvmptv  5209  iunopab  5534  dfid4  5547  dfid2  5548  dfid3  5549  rabxp  5699  fconstmpt  5713  csbxp  5752  cnvi  5863  cnvco  5867  csbdm  5879  rnmpt  5939  csbres  5973  resundi  5984  resundir  5985  resindi  5986  resindir  5987  rescom  5993  resima  6056  imadmrnOLD  6068  cnvimarndmOLD  6081  cnvin  6135  rnun  6136  imaundi  6141  cnvxpOLD  6148  imainrect  6173  csbrn  6204  imacnvcnv  6207  resdmres  6233  imadmres  6235  resdifdir  6238  mptpreima  6239  dfpred3  6315  predin  6330  predun  6331  preddif  6332  frpoind  6345  cbviotaw  6501  cbviotavw  6502  cbviota  6503  sb8iota  6505  resdif  6846  opabiotadm  6966  fndmin  7044  fninfp  7179  cbvriotaw  7386  cbvriotavw  7387  cbvriota  7390  riotarab  7419  dfoprab2  7478  cbvoprab1  7507  cbvoprab2  7508  cbvoprab12  7509  cbvoprab12v  7510  cbvoprab3  7511  cbvoprab3v  7512  cbvmpox  7513  cbvmpov  7515  resoprab  7538  caov32  7648  caov31  7650  caov4  7652  caovlem2  7657  mpt3mpt  7685  uniuni  7776  zfrep6OLD  7967  ofmres  7996  dfopab2  8063  dfxp3  8072  dmmpossx  8077  fmpox  8078  fsplit  8128  ovtpos  8258  tposco  8274  frrlem5  8308  tfrlem10  8395  o2p2e4  8549  0map0sn0  8913  mapsncnv  8921  cbvixp  8942  cbvixpv  8943  xpcomco  9086  sbthlem6  9111  ttrclresv  9718  frind  9754  cardf2  10024  alephcard  10149  alephfplem1  10183  xp2dju  10255  djuassen  10257  infdju1  10268  pwdju1  10269  ackbij1lem14  10310  compsscnv  10449  dffin1-5  10466  ituniiun  10500  axdc2lem  10526  axdc3lem4  10531  axcclem  10535  pwcfsdom  10668  dmaddpi  10975  dmmulpi  10976  adderpqlem  11039  addassnq  11043  mulcanenq  11045  addcmpblnr  11154  mulcmpblnrlem  11155  ltsrpr  11162  mulgt0sr  11190  sqgt0sr  11191  axi2m1  11244  negiso  12297  nummac  12864  decsubi  12882  9t11e99OLD  12950  fztpval  13720  seqval  14155  sqrecii  14326  sqdivi  14328  binom2i  14356  4bc2eq6  14473  hashgval  14477  revs1  14914  cats1cat  15012  trclublem  15148  shftdm  15224  shftidt2  15234  cji  15326  cbvsum  15862  cbvsumv  15863  sumfc  15875  ackbijnn  15997  cbvprod  16082  cbvprodv  16083  prodeq1i  16085  prodfc  16112  fsumcube  16226  divalglem2  16565  nn0expgcd  16738  nn0gcdsq  16928  prmreclem2  17095  prmrec  17100  hashbc0  17183  dec5nprm  17244  dec2nprm  17245  gcdi  17251  decsplit  17260  1259lem1  17309  1259lem4  17312  4001lem1  17319  phlstr  17517  oduval  18462  oduleval  18463  odubas  18465  lubdm  18523  glbdm  18536  degenmgmopdm  19134  degenmgm2opdm  19138  oppgid  19570  symgbas0  19603  gsumcom2  20189  ringidval  20409  oppr1  20580  dfrhm2  20704  rmodislmod  21205  cnfldsub  21706  cnflddiv  21708  dvdsrzring  21767  pjdm  22013  pjfval2  22015  opsrtoslem1  22364  restco  23482  ufprim  24228  tgioo3  25125  oprpiece1res1  25272  oprpiece1res2  25273  volfiniun  25868  vitalilem4  25932  cbvitg  26096  cbvitgv  26097  itgresr  26099  cbvditg  26174  plyid  26527  coeidp  26582  dgrid  26583  sincos3rdpi  26845  logblog  27120  ang180lem2  27138  1cubrlem  27169  asin1  27222  log2ublem2  27275  log2ublem3  27276  emcllem5  27327  lgsdir2lem5  27656  lgsquadlem3  27709  2lgslem1b  27719  2lgsoddprmlem3d  27740  noextend  28023  nosupbday  28062  nosupbnd1  28071  nosupbnd2  28073  noinfbday  28077  noinfbnd1  28086  dmcuts  28177  madeval2  28219  neg0s  28412  neg1s  28413  cchhllem  29464  ax5seglem7  29513  vtxval0  29617  iedgval0  29618  finsumvtxdg2ssteplem1  30126  wwlksnfi  30495  1wlkdlem1  30728  ex-un  31025  ex-pw  31030  ex-cnv  31038  ex-co  31039  bafval  31206  vsfval  31235  cnnvba  31281  cnnvm  31284  ip2dii  31446  siilem1  31453  h2hcau  31581  hvsubsub4i  31661  hvnegdii  31664  normlem3  31714  normlem8  31719  norm-iii-i  31741  normpar2i  31758  polid2i  31759  chjassi  32088  chj4i  32125  h1de2i  32155  spanunsni  32181  fh3i  32225  fh4i  32226  qlax4i  32232  qlaxr3i  32238  3oalem5  32268  pjadjii  32276  pjsubii  32280  hoadd32i  32380  cnvadj  32494  hh0oi  32505  hhcno  32506  hhcnf  32507  nmopnegi  32567  lnophmlem2  32619  branmfn  32707  dmrab  33093  3unrab  33099  abrexexd  33105  cbviunf  33150  maprnin  33323  dpmul10  33461  dpexpp1  33474  dpadd3  33478  dpmul  33479  dpmul4  33480  psgnfzto1st  33666  cycpmconjs  33717  fracbas  33867  cos9thpiminplylem5  34418  lmlimxrge0  34580  zrhre  34651  qqhre  34652  rrhre  34653  cbvesum  34674  cbvesumv  34675  unibrsiga  34819  eulerpartlemt  35003  eulerpartgbij  35004  ballotlemrinv  35166  hgt750lem2  35281  bnj1146  35421  bnj893  35558  bnj1234  35643  r11  35725  r12  35726  subfacp1lem1  35944  kur14lem2  35972  kur14lem5  35975  kur14lem7  35977  cvmscld  36038  satfv1lem  36127  fmla0  36147  mvtval  36265  mthmpps  36347  fixun  36671  rabeqbii  36983  iuneq12i  36984  iineq1i  36985  iineq12i  36986  riotaeqbii  36987  ixpeq1i  36989  sumeq2si  36991  prodeq2si  36993  itgeq12i  36995  ditgeq123i  36998  cbvcsbvw2  37020  cbviunvw2  37021  cbviinvw2  37022  cbvmptvw2  37023  cbvriotavw2  37025  cbvoprab1vw  37026  cbvoprab2vw  37027  cbvoprab123vw  37028  cbvoprab23vw  37029  cbvoprab13vw  37030  cbvmpovw2  37031  cbvmpo1vw2  37032  cbvmpo2vw2  37033  cbvixpvw2  37034  cbvprodvw2  37036  cbvitgvw2  37037  cbvditgvw2  37038  ttcun  37300  ttciun  37302  bj-inrab  37840  bj-inrab3  37842  bj-gabeqis  37851  bj-pr1un  37916  bj-pr2un  37930  bj-dfid2ALT  37980  bj-mpomptALT  38040  rnmptsn  38258  f1omptsnlem  38259  rabiun  38521  phpreu  38527  poimirlem18  38556  ovoliunnfl  38580  voliunnfl  38582  mbfposadd  38585  asindmre  38621  abeqin  39186  rncnvepres  39241  qsresid  39263  dmxrn  39319  rnxrn  39353  xrnres  39357  xrnres2  39358  xrnres3  39359  dmxrncnvepres2  39365  dfsucmap3  39395  dfsucmap2  39396  rncossdmcoss  39477  1cosscnvxrn  39497  refrelsredund4  39648  mpets  39888  dfpetparts2  39904  dfpeters2  39906  petseq  39908  pets2eq  39909  cdleme25cv  41415  sn-iotalemcor  43276  sqdeccom12  43346  sumcubes  43370  resuppsinopn  43414  sn-00idlem2  43450  sn-1ticom  43486  mendsca  44186  areaquad  44217  onsucrn  44272  df3o2  44314  df3o3  44315  omcl3g  44335  dfno2  44428  cnvrcl0  44624  sqrtcvallem1  44630  trclrelexplem  44710  iuneq1i  46100  cbvmpo2  46111  cbvmpo1  46112  cbvrabv2w  46142  mptssid  46252  fprodabs2  46606  stoweidlem13  47022  wallispilem4  47077  fourierdlem94  47209  fourierdlem102  47217  fourierdlem111  47226  fourierdlem112  47227  fourierdlem113  47228  fourierdlem114  47229  41prothprmlem2  48702  2exp340mod341  48830  8exp8mod9  48833  nfermltl8rev  48839  stgr1  49058  gpgprismgr4cycllem6  49197  gpgprismgr4cycllem9  49200  gpgprismgr4cycllem10  49201  cbvmpox2  49447  dmmpossx2  49448  zlmodzxzequa  49607  zlmodzxzequap  49610  resinsn  49979  dfswapf2  50368