Theorem 3eqtr3i 2760

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  un12  4124  in12  4180  indif1  4233  difundi  4241  difundir  4242  difindi  4243  difindir  4244  dif32  4253  csbvarg  4385  undif1  4427  resmpt3  5989  xp0  6107  partfun  6629  fresaunres2  6696  caov12  7577  caov13  7579  caov411  7581  caovdir  7583  orduniss2  7766  fparlem3  8047  fparlem4  8048  fsplitfpar  8051  hartogslem1  9434  ttrclco  9614  kmlem3  10047  djuassen  10073  xpdjuen  10074  halfnq  10870  reclem3pr  10943  addcmpblnr  10963  ltsrpr  10971  pn0sr  10995  sqgt0sr  11000  map2psrpr  11004  negsubdii  11449  i4  14111  nn0opthlem1  14175  fac4  14188  imi  15064  bpoly3  15965  ef01bndlem  16093  bitsres  16384  gcdaddmlem  16435  modsubi  16984  gcdmodi  16986  numexpp1  16989  karatsuba  16995  oppgcntr  19244  frgpuplem  19651  0frgp  19658  pzriprnglem11  21398  ressmpladd  21934  ressmplmul  21935  ressmplvsca  21936  ltbwe  21949  ressply1add  22112  ressply1mul  22113  ressply1vsca  22114  sn0cld  22975  qtopres  23583  itg1addlem5  25599  cospi  26379  sincos4thpi  26420  sincos3rdpi  26424  dvlog  26558  dvlog2  26560  dvsqrt  26649  dvcnsqrt  26651  ang180lem3  26719  1cubrlem  26749  mcubic  26755  quart1lem  26763  atantayl2  26846  log2cnv  26852  log2ublem2  26855  log2ub  26857  gam1  26973  chtub  27121  bclbnd  27189  bposlem8  27200  lgsdir2lem1  27234  lgsdir2lem5  27238  2lgsoddprmlem3d  27322  ex-bc  30396  ex-gcd  30401  ipidsq  30654  ip1ilem  30770  ipdirilem  30773  ipasslem10  30783  siilem1  30795  hvmul2negi  30992  hvadd12i  31001  hvnegdii  31006  normlem1  31054  normlem9  31062  normsubi  31085  normpar2i  31100  polid2i  31101  chjassi  31430  chj12i  31466  pjoml2i  31529  hoadd12i  31721  lnophmlem2  31961  nmopcoadj2i  32046  indifundif  32468  aciunf1  32607  fressupp  32631  ffsrn  32673  dpmul10  32836  dpmul1000  32840  dpadd2  32851  dpadd  32852  dpmul  32854  cycpmconjslem1  33097  archirngz  33132  psrbasfsupp  33545  cos9thpiminplylem4  33758  cos9thpiminplylem5  33759  sqsscirc1  33881  sigaclfu2  34094  eulerpartlemd  34340  coinflippvt  34459  ballotth  34512  hgt750lem  34625  hgt750lem2  34626  quad3  35653  onint1  36433  bj-csbsn  36888  cnambfre  37658  sqmid3api  42266  sin2t3rdpi  42336  cos2t3rdpi  42337  sin4t3rdpi  42338  cos4t3rdpi  42339  redvmptabs  42343  re1m1e0m0  42380  sn-1ticom  42418  rabren3dioph  42798  arearect  43198  areaquad  43199  resnonrel  43575  cononrel1  43577  cononrel2  43578  lhe4.4ex1a  44312  expgrowthi  44316  expgrowth  44318  binomcxplemnotnn0  44339  liminf0  45784  dvcosre  45903  stoweidlem34  46025  fouriersw  46222  ceil5half3  47334  tposresg  48872  tposideq  48882