Theorem 3eqtr3i 2791

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 2785	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2785	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 2155  ax-ext 2732

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

This theorem is used by:  un12  4119  in12  4174  indif1  4228  difundi  4236  difundir  4237  difindi  4238  difindir  4239  dif32  4248  csbvarg  4392  undif1  4430  unidif0  5324  resmpt3  6035  xp0OLD  6151  partfun  6681  fresaunres2  6749  caov12  7644  caov13  7646  caov411  7648  caovdir  7650  orduniss2  7831  fparlem3  8113  fparlem4  8114  fsplitfpar  8117  hartogslem1  9518  ttrclco  9701  kmlem3  10177  djuassen  10203  xpdjuen  10204  halfnq  11007  reclem3pr  11080  addcmpblnr  11100  ltsrpr  11108  pn0sr  11132  sqgt0sr  11137  map2psrpr  11141  negsubdii  11589  8th4div3  12510  i4  14290  nn0opthlem1  14354  fac4  14367  imi  15266  bpoly3  16166  ef01bndlem  16294  bitsres  16585  gcdaddmlem  16636  modsubi  17186  gcdmodi  17188  numexpp1  17191  karatsuba  17197  oppgcntr  19515  frgpuplem  19922  0frgp  19929  pzriprnglem11  21733  ressmpladd  22273  ressmplmul  22274  ressmplvsca  22275  ltbwe  22289  ressply1add  22483  ressply1mul  22484  ressply1vsca  22485  sn0cld  23344  qtopres  23953  itg1addlem5  25957  cospi  26739  sincos4thpi  26780  sincos3rdpi  26783  dvlog  26917  dvlog2  26919  dvsqrt  27008  dvcnsqrt  27010  ang180lem3  27077  1cubrlem  27107  mcubic  27113  quart1lem  27121  atantayl2  27204  log2cnv  27210  log2ublem2  27213  log2ub  27215  gam1  27330  chtub  27477  bclbnd  27545  bposlem8  27556  lgsdir2lem1  27590  lgsdir2lem5  27594  2lgsoddprmlem3d  27678  ex-bc  30961  ex-gcd  30966  ipidsq  31220  ip1ilem  31336  ipdirilem  31339  ipasslem10  31349  siilem1  31361  hvmul2negi  31558  hvadd12i  31567  hvnegdii  31572  normlem1  31620  normlem9  31628  normsubi  31651  normpar2i  31666  polid2i  31667  chjassi  31996  chj12i  32032  pjoml2i  32095  hoadd12i  32287  lnophmlem2  32527  nmopcoadj2i  32612  indifundif  33028  ififcom  33054  aciunf1  33165  partfun2  33178  fressupp  33189  ffsrn  33228  dpmul10  33369  dpmul1000  33373  dpadd2  33384  dpadd  33385  dpmul  33387  cycpmconjslem1  33623  archirngz  33658  psrbasfsupp  34051  cos9thpiminplylem4  34325  cos9thpiminplylem5  34326  sqsscirc1  34448  sigaclfu2  34661  eulerpartlemd  34907  coinflippvt  35026  ballotth  35079  hgt750lem  35189  hgt750lem2  35190  quad3  36279  onint1  37082  bj-csbsn  37661  cnambfre  38431  vxp  39025  sqmid3api  43172  sin2t3rdpi  43242  cos2t3rdpi  43243  sin4t3rdpi  43244  cos4t3rdpi  43245  redvmptabs  43249  re1m1e0m0  43286  sn-1ticom  43324  rabren3dioph  43670  arearect  44070  areaquad  44071  resnonrel  44446  cononrel1  44448  cononrel2  44449  lhe4.4ex1a  45167  expgrowthi  45171  expgrowth  45173  binomcxplemnotnn0  45194  liminf0  46635  dvcosre  46754  stoweidlem34  46876  fouriersw  47073  goldratmolem2  47765  ceil5half3  48248  tposresg  49818  tposideq  49828  veroquadgsumlem  50830