Theorem 3eqtr3i 2761

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

Syntax hints:   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717

This theorem is referenced by:  un12  4165  in12  4219  indif1  4270  difundi  4278  difundir  4279  difindi  4280  difindir  4281  dif32  4291  csbvarg  4433  undif1  4477  resmpt3  6043  xp0  6164  partfun  6703  fresaunres2  6769  caov12  7649  caov13  7651  caov411  7653  caovdir  7655  orduniss2  7837  fparlem3  8119  fparlem4  8120  fsplitfpar  8123  hartogslem1  9567  ttrclco  9743  kmlem3  10177  djuassen  10203  xpdjuen  10204  halfnq  11001  reclem3pr  11074  addcmpblnr  11094  ltsrpr  11102  pn0sr  11126  sqgt0sr  11131  map2psrpr  11135  negsubdii  11577  halfpm6th  12466  i4  14203  nn0opthlem1  14263  fac4  14276  imi  15140  bpoly3  16038  ef01bndlem  16164  bitsres  16451  gcdaddmlem  16502  modsubi  17044  gcdmodi  17046  numexpp1  17050  karatsuba  17056  oppgcntr  19331  frgpuplem  19739  0frgp  19746  pzriprnglem11  21434  ressmpladd  21989  ressmplmul  21990  ressmplvsca  21991  ltbwe  22004  ressply1add  22172  ressply1mul  22173  ressply1vsca  22174  sn0cld  23038  qtopres  23646  itg1addlem5  25674  cospi  26452  sincos4thpi  26493  sincos3rdpi  26496  dvlog  26630  dvlog2  26632  dvsqrt  26721  dvcnsqrt  26723  ang180lem3  26788  1cubrlem  26818  mcubic  26824  quart1lem  26832  atantayl2  26915  log2cnv  26921  log2ublem2  26924  log2ub  26926  gam1  27042  chtub  27190  bclbnd  27258  bposlem8  27269  lgsdir2lem1  27303  lgsdir2lem5  27307  2lgsoddprmlem3d  27391  ex-bc  30334  ex-gcd  30339  ipidsq  30592  ip1ilem  30708  ipdirilem  30711  ipasslem10  30721  siilem1  30733  hvmul2negi  30930  hvadd12i  30939  hvnegdii  30944  normlem1  30992  normlem9  31000  normsubi  31023  normpar2i  31038  polid2i  31039  chjassi  31368  chj12i  31404  pjoml2i  31467  hoadd12i  31659  lnophmlem2  31899  nmopcoadj2i  31984  indifundif  32400  aciunf1  32530  fressupp  32550  ffsrn  32593  dpmul10  32703  dpmul1000  32707  dpadd2  32718  dpadd  32719  dpmul  32721  cycpmconjslem1  32967  archirngz  32989  sqsscirc1  33640  sigaclfu2  33871  eulerpartlemd  34117  coinflippvt  34235  ballotth  34288  hgt750lem  34414  hgt750lem2  34415  quad3  35405  onint1  36064  bj-csbsn  36513  cnambfre  37272  sqmid3api  41992  re1m1e0m0  42087  sn-1ticom  42124  rabren3dioph  42377  arearect  42785  areaquad  42786  resnonrel  43164  cononrel1  43166  cononrel2  43167  lhe4.4ex1a  43908  expgrowthi  43912  expgrowth  43914  binomcxplemnotnn0  43935  liminf0  45319  dvcosre  45438  stoweidlem34  45560  fouriersw  45757