Theorem 3eqtr4i 1921

Description: An inference from three chained equalities. (The proof was shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr4i.1	|- A = B
3eqtr4i.2	|- C = A
3eqtr4i.3	|- D = B

Assertion

Ref	Expression
3eqtr4i	|- C = D

Proof of Theorem 3eqtr4i

Step	Hyp	Ref	Expression
1		3eqtr4i.2	. 2 |- C = A
2		3eqtr4i.3	. . 3 |- D = B
3		3eqtr4i.1	. . 3 |- A = B
4	2, 3	eqtr4i 1911	. 2 |- D = A
5	1, 4	eqtr4i 1911	1 |- C = D

Syntax hints:   = wceq 1298

This theorem is referenced by:  rabswap 2256  rabbiia 2285  cbvrab 2421  un23OLD 2763  un4 2764  in23OLD 2807  in4 2808  indir 2842  undir 2843  unrab 2865  inrab 2866  inrab2 2867  difrab 2868  dfnul3 2878  rab0 2894  difdifdir 2957  prcom 3097  pw0 3132  pwpw0 3134  pwsn 3172  pwsnALT 3173  int0 3230  dfiin2OLD 3288  iinab 3317  iunun 3328  cbvopab 3403  cbvopab1 3405  cbvopab1s 3406  cbvopab2v 3408  unopab 3410  uniuni 3806  dfom2 3951  xpundi 4050  xpundir 4051  inxp 4109  cnvco 4145  cnvcoOLD 4146  dm0OLD 4171  dmiOLD 4173  resundi 4229  resundir 4230  resindi 4231  resindir 4232  rescom 4238  resima 4247  imadmrn 4277  cnvi 4320  rnun 4325  imaundi 4328  cnvxp 4332  dmprop 4369  rescnvcnvOLD 4386  imacnvcnv 4388  resdmres 4390  imadmres 4391  co01 4412  iunfopab 4542  zfrep6 4545  resdif 4659  dfoprab2 4917  cbvoprab1 4924  cbvoprab1OLD 4925  cbvoprab12 4926  cbvoprab12OLD 4927  cbvoprab3v 4929  resoprab 4938  caopr32 4993  caopr31 4995  caopr4 4997  caoprlem2 5002  cbvmpt 5011  fo1st 5032  fo2nd 5033  foprab2 5061  fparlem2 5082  tfrlem10 5128  tz7.44-2 5137  tz7.44-3 5138  rdglem2 5146  frfnom 5159  dfec2 5321  snec 5355  map0e 5401  sbthlem6 5515  unfilem1 5641  abfii5 5655  ranksn 5800  rankelun 5818  numthlem 5945  alephcard 6015  xp2cda 6078  dmaddpi 6170  dmmulpi 6171  addasspq 6215  genpdm 6257  prlem936 6307  m1p1sr 6353  m1m1sr 6354  mulgt0sr 6366  axi2m1 6438  mulneg1i 6608  divdiri 6930  divdiv23i 6970  3p3e6 7192  4p3e7 7194  4p4e8 7195  5p3e8 7197  5p4e9 7198  5p5e10 7199  6p3e9 7201  6p4e10 7202  7p3e10 7204  fzprval 7687  fztpval 7688  cardfz 7719  seq1res 7740  seq1shftid 7769  sqdivi 7863  sqrecii 7864  binom2i 7890  sqr0 7922  sqrlem16 7938  crmuli 7990  cjcji 8028  readdi 8034  imaddi 8035  cjaddi 8038  cjmuli 8039  cjmulrcli 8041  renegi 8044  imnegi 8046  cjnegi 8047  addcji 8048  cji 8077  absmuli 8098  absi 8130  faclbnd4lem1 8200  bcpasc2i 8219  cbvsumi 8246  ser1consti 8431  geoseri 8496  geolim1i 8500  eirrlem3 8653  eirrlem5 8655  efsepi 8661  efcnlem2 8685  sinaddi 8716  cosaddi 8717  cos2OLD 8730  bafval 9555  0vfval 9557  vsfval 9586  cnnvba 9641  cnnvm 9645  ipasslem10 9840  ip2dii 9845  siilem1 9852  efghgrpilem 10073  pilog 10122  cvimarndm 10151  oprabopabf 10157  zrdivrng 10418  h2hcau 10481  h2hlm 10482  hvsubassi 10554  hvsub23i 10555  hvsubsub4i 10558  hvnegdii 10561  his35i 10588  normlem3 10611  normlem8 10616  norm-iii.i 10639  norm3difi 10647  normpari 10654  normpar2i 10656  polid2i 10657  hhssims 10778  occllem1 10806  projlem3 10821  chjassi 11042  chj4i 11079  h1de2i 11109  spanunsni 11135  fh3i 11199  fh4i 11200  qlax4i 11206  qlaxr3i 11212  3oalem5 11246  pjadjii 11253  pjsubii 11258  pjcji 11264  pjrni 11282  hoadd23i 11341  dfbdop2 11423  cnvadj 11453  hhlnoi 11463  bra0 11511  nmopnegi 11526  lnopunilem1 11572  lnophmlem2 11579  branmfn 11675  branmfnOLD 11676  bnj884 12809  bnj888 12811  bnj1146 12943  bnj1273 13029  bnj1401 13113  bnj96 13219  bnj1234 13460  bnj1387 13526  divalglem2 13698  mulgcdlem2 13757  mpteqi 13838  predidm 13899  predin 13900  predun 13901  preddif 13902  wfi 13915  frind 13939  orkurss 14488  cbvprodi 14662  subspemp 14903  limfillem2 14939  singempcon 14965  idtrgrp 14978  cnvtr 15016  mamb 15030  cbviin 15357  cbvoprab2 15708  cbvixp 15723  piececn 15894  heiborlem42 15996  ismrer1 16024  pcocn 16076  cbvrabcsf 16414  cbviotaf 16432  stbbi 16726  stb2xpl 16742  stb3xpl 16743  isgrpiNEW 17115

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain