Theorem 3eqtr3i 2768

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

Hypotheses

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

Assertion

Ref	Expression
3eqtr3i	⊢ 𝐶 = 𝐷

Proof of Theorem 3eqtr3i

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  un12  4167  in12  4220  indif1  4271  difundi  4279  difundir  4280  difindi  4281  difindir  4282  dif32  4292  csbvarg  4431  undif1  4475  resmpt3  6038  xp0  6157  partfun  6697  fresaunres2  6763  caov12  7637  caov13  7639  caov411  7641  caovdir  7643  orduniss2  7823  fparlem3  8102  fparlem4  8103  fsplitfpar  8106  hartogslem1  9539  ttrclco  9715  kmlem3  10149  djuassen  10175  xpdjuen  10176  halfnq  10973  reclem3pr  11046  addcmpblnr  11066  ltsrpr  11074  pn0sr  11098  sqgt0sr  11103  map2psrpr  11107  negsubdii  11549  halfpm6th  12437  i4  14172  nn0opthlem1  14232  fac4  14245  imi  15108  bpoly3  16006  ef01bndlem  16131  bitsres  16418  gcdaddmlem  16469  modsubi  17009  gcdmodi  17011  numexpp1  17015  karatsuba  17021  oppgcntr  19273  frgpuplem  19681  0frgp  19688  pzriprnglem11  21260  ressmpladd  21803  ressmplmul  21804  ressmplvsca  21805  ltbwe  21818  ressply1add  21972  ressply1mul  21973  ressply1vsca  21974  sn0cld  22814  qtopres  23422  itg1addlem5  25442  cospi  26206  sincos4thpi  26247  sincos3rdpi  26250  dvlog  26383  dvlog2  26385  dvsqrt  26474  dvcnsqrt  26476  ang180lem3  26540  1cubrlem  26570  mcubic  26576  quart1lem  26584  atantayl2  26667  log2cnv  26673  log2ublem2  26676  log2ub  26678  gam1  26793  chtub  26939  bclbnd  27007  bposlem8  27018  lgsdir2lem1  27052  lgsdir2lem5  27056  2lgsoddprmlem3d  27140  ex-bc  29960  ex-gcd  29965  ipidsq  30218  ip1ilem  30334  ipdirilem  30337  ipasslem10  30347  siilem1  30359  hvmul2negi  30556  hvadd12i  30565  hvnegdii  30570  normlem1  30618  normlem9  30626  normsubi  30649  normpar2i  30664  polid2i  30665  chjassi  30994  chj12i  31030  pjoml2i  31093  hoadd12i  31285  lnophmlem2  31525  nmopcoadj2i  31610  indifundif  32017  aciunf1  32143  fressupp  32165  ffsrn  32209  dpmul10  32316  dpmul1000  32320  dpadd2  32331  dpadd  32332  dpmul  32334  cycpmconjslem1  32571  archirngz  32593  sqsscirc1  33174  sigaclfu2  33405  eulerpartlemd  33651  coinflippvt  33769  ballotth  33822  hgt750lem  33949  hgt750lem2  33950  quad3  34941  onint1  35637  bj-csbsn  36087  cnambfre  36839  sqmid3api  41497  re1m1e0m0  41572  sn-1ticom  41609  rabren3dioph  41855  arearect  42266  areaquad  42267  resnonrel  42645  cononrel1  42647  cononrel2  42648  lhe4.4ex1a  43390  expgrowthi  43394  expgrowth  43396  binomcxplemnotnn0  43417  liminf0  44808  dvcosre  44927  stoweidlem34  45049  fouriersw  45246