Theorem 3eqtr3i 2776

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 2770	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2770	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 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  un12  4196  in12  4250  indif1  4301  difundi  4309  difundir  4310  difindi  4311  difindir  4312  dif32  4321  csbvarg  4457  undif1  4499  resmpt3  6067  xp0  6189  partfun  6727  fresaunres2  6793  caov12  7678  caov13  7680  caov411  7682  caovdir  7684  orduniss2  7869  fparlem3  8155  fparlem4  8156  fsplitfpar  8159  hartogslem1  9611  ttrclco  9787  kmlem3  10222  djuassen  10248  xpdjuen  10249  halfnq  11045  reclem3pr  11118  addcmpblnr  11138  ltsrpr  11146  pn0sr  11170  sqgt0sr  11175  map2psrpr  11179  negsubdii  11621  halfpm6th  12514  i4  14253  nn0opthlem1  14317  fac4  14330  imi  15206  bpoly3  16106  ef01bndlem  16232  bitsres  16519  gcdaddmlem  16570  modsubi  17119  gcdmodi  17121  numexpp1  17125  karatsuba  17131  oppgcntr  19408  frgpuplem  19814  0frgp  19821  pzriprnglem11  21525  ressmpladd  22070  ressmplmul  22071  ressmplvsca  22072  ltbwe  22085  ressply1add  22252  ressply1mul  22253  ressply1vsca  22254  sn0cld  23119  qtopres  23727  itg1addlem5  25755  cospi  26532  sincos4thpi  26573  sincos3rdpi  26577  dvlog  26711  dvlog2  26713  dvsqrt  26802  dvcnsqrt  26804  ang180lem3  26872  1cubrlem  26902  mcubic  26908  quart1lem  26916  atantayl2  26999  log2cnv  27005  log2ublem2  27008  log2ub  27010  gam1  27126  chtub  27274  bclbnd  27342  bposlem8  27353  lgsdir2lem1  27387  lgsdir2lem5  27391  2lgsoddprmlem3d  27475  ex-bc  30484  ex-gcd  30489  ipidsq  30742  ip1ilem  30858  ipdirilem  30861  ipasslem10  30871  siilem1  30883  hvmul2negi  31080  hvadd12i  31089  hvnegdii  31094  normlem1  31142  normlem9  31150  normsubi  31173  normpar2i  31188  polid2i  31189  chjassi  31518  chj12i  31554  pjoml2i  31617  hoadd12i  31809  lnophmlem2  32049  nmopcoadj2i  32134  indifundif  32554  aciunf1  32681  fressupp  32700  ffsrn  32743  dpmul10  32859  dpmul1000  32863  dpadd2  32874  dpadd  32875  dpmul  32877  cycpmconjslem1  33147  archirngz  33169  sqsscirc1  33854  sigaclfu2  34085  eulerpartlemd  34331  coinflippvt  34449  ballotth  34502  hgt750lem  34628  hgt750lem2  34629  quad3  35638  onint1  36415  bj-csbsn  36870  cnambfre  37628  sqmid3api  42272  re1m1e0m0  42373  sn-1ticom  42410  rabren3dioph  42771  arearect  43176  areaquad  43177  resnonrel  43554  cononrel1  43556  cononrel2  43557  lhe4.4ex1a  44298  expgrowthi  44302  expgrowth  44304  binomcxplemnotnn0  44325  liminf0  45714  dvcosre  45833  stoweidlem34  45955  fouriersw  46152