Theorem 3eqtr3i 2796

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  un12  4126  in12  4181  indif1  4235  difundi  4243  difundir  4244  difindi  4245  difindir  4246  dif32  4255  csbvarg  4399  undif1  4437  unidif0  5332  resmpt3  6042  xp0OLD  6158  partfun  6687  fresaunres2  6755  caov12  7649  caov13  7651  caov411  7653  caovdir  7655  orduniss2  7836  fparlem3  8116  fparlem4  8117  fsplitfpar  8120  hartogslem1  9512  ttrclco  9695  kmlem3  10153  djuassen  10179  xpdjuen  10180  halfnq  10981  reclem3pr  11054  addcmpblnr  11074  ltsrpr  11082  pn0sr  11106  sqgt0sr  11111  map2psrpr  11115  negsubdii  11563  8th4div3  12484  i4  14263  nn0opthlem1  14327  fac4  14340  imi  15237  bpoly3  16139  ef01bndlem  16267  bitsres  16558  gcdaddmlem  16609  modsubi  17159  gcdmodi  17161  numexpp1  17164  karatsuba  17170  oppgcntr  19484  frgpuplem  19891  0frgp  19898  pzriprnglem11  21696  ressmpladd  22234  ressmplmul  22235  ressmplvsca  22236  ltbwe  22250  ressply1add  22444  ressply1mul  22445  ressply1vsca  22446  sn0cld  23302  qtopres  23911  itg1addlem5  25915  cospi  26693  sincos4thpi  26734  sincos3rdpi  26738  dvlog  26872  dvlog2  26874  dvsqrt  26963  dvcnsqrt  26965  ang180lem3  27032  1cubrlem  27062  mcubic  27068  quart1lem  27076  atantayl2  27159  log2cnv  27165  log2ublem2  27168  log2ub  27170  gam1  27285  chtub  27432  bclbnd  27500  bposlem8  27511  lgsdir2lem1  27545  lgsdir2lem5  27549  2lgsoddprmlem3d  27633  ex-bc  30879  ex-gcd  30884  ipidsq  31138  ip1ilem  31254  ipdirilem  31257  ipasslem10  31267  siilem1  31279  hvmul2negi  31476  hvadd12i  31485  hvnegdii  31490  normlem1  31538  normlem9  31546  normsubi  31569  normpar2i  31584  polid2i  31585  chjassi  31914  chj12i  31950  pjoml2i  32013  hoadd12i  32205  lnophmlem2  32445  nmopcoadj2i  32530  indifundif  32946  ififcom  32972  aciunf1  33084  partfun2  33097  fressupp  33109  ffsrn  33148  dpmul10  33289  dpmul1000  33293  dpadd2  33304  dpadd  33305  dpmul  33307  cycpmconjslem1  33543  archirngz  33578  psrbasfsupp  33970  cos9thpiminplylem4  34244  cos9thpiminplylem5  34245  sqsscirc1  34367  sigaclfu2  34580  eulerpartlemd  34826  coinflippvt  34945  ballotth  34998  hgt750lem  35108  hgt750lem2  35109  quad3  36204  onint1  37022  bj-csbsn  37601  cnambfre  38381  vxp  38975  sqmid3api  43122  sin2t3rdpi  43192  cos2t3rdpi  43193  sin4t3rdpi  43194  cos4t3rdpi  43195  redvmptabs  43199  re1m1e0m0  43236  sn-1ticom  43274  rabren3dioph  43620  arearect  44020  areaquad  44021  resnonrel  44396  cononrel1  44398  cononrel2  44399  lhe4.4ex1a  45117  expgrowthi  45121  expgrowth  45123  binomcxplemnotnn0  45144  liminf0  46585  dvcosre  46704  stoweidlem34  46826  fouriersw  47023  goldratmolem2  47701  ceil5half3  48161  tposresg  49733  tposideq  49743