Theorem 3eqtr3i 2854

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 2848	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2848	1 ⊢ 𝐶 = 𝐷

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816

This theorem is referenced by:  un12  4145  in12  4199  indif1  4250  difundi  4258  difundir  4259  difindi  4260  difindir  4261  dif32  4269  csbvarg  4385  undif1  4426  resmpt3  5908  xp0  6017  fresaunres2  6552  caov12  7378  caov13  7380  caov411  7382  caovdir  7384  orduniss2  7550  fparlem3  7811  fparlem4  7812  fsplitfpar  7816  hartogslem1  9008  kmlem3  9580  djuassen  9606  xpdjuen  9607  halfnq  10400  reclem3pr  10473  addcmpblnr  10493  ltsrpr  10501  pn0sr  10525  sqgt0sr  10530  map2psrpr  10534  negsubdii  10973  halfpm6th  11861  i4  13570  nn0opthlem1  13631  fac4  13644  imi  14518  bpoly3  15414  ef01bndlem  15539  bitsres  15824  gcdaddmlem  15874  modsubi  16410  gcdmodi  16412  numexpp1  16416  karatsuba  16422  oppgcntr  18495  frgpuplem  18900  0frgp  18907  ressmpladd  20240  ressmplmul  20241  ressmplvsca  20242  ltbwe  20255  ressply1add  20400  ressply1mul  20401  ressply1vsca  20402  sn0cld  21700  qtopres  22308  itg1addlem5  24303  cospi  25060  sincos4thpi  25101  sincos3rdpi  25104  dvlog  25236  dvlog2  25238  dvsqrt  25325  dvcnsqrt  25327  ang180lem3  25391  1cubrlem  25421  mcubic  25427  quart1lem  25435  atantayl2  25518  log2cnv  25524  log2ublem2  25527  log2ub  25529  gam1  25644  chtub  25790  bclbnd  25858  bposlem8  25869  lgsdir2lem1  25903  lgsdir2lem5  25907  2lgsoddprmlem3d  25991  ex-bc  28233  ex-gcd  28238  ipidsq  28489  ip1ilem  28605  ipdirilem  28608  ipasslem10  28618  siilem1  28630  hvmul2negi  28827  hvadd12i  28836  hvnegdii  28841  normlem1  28889  normlem9  28897  normsubi  28920  normpar2i  28935  polid2i  28936  chjassi  29265  chj12i  29301  pjoml2i  29364  hoadd12i  29556  lnophmlem2  29796  nmopcoadj2i  29881  indifundif  30287  aciunf1  30410  partfun  30423  ffsrn  30467  dpmul10  30573  dpmul1000  30577  dpadd2  30588  dpadd  30589  dpmul  30591  cycpmconjslem1  30798  archirngz  30820  sqsscirc1  31153  sigaclfu2  31382  eulerpartlemd  31626  coinflippvt  31744  ballotth  31797  hgt750lem  31924  hgt750lem2  31925  quad3  32915  onint1  33799  bj-csbsn  34223  cnambfre  34942  sqmid3api  39176  re1m1e0m0  39234  rabren3dioph  39419  arearect  39829  areaquad  39830  resnonrel  39959  cononrel1  39961  cononrel2  39962  lhe4.4ex1a  40668  expgrowthi  40672  expgrowth  40674  binomcxplemnotnn0  40695  liminf0  42081  dvcosre  42203  stoweidlem34  42326  fouriersw  42523