Theorem 3eqtr3i 2772

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

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728

This theorem is referenced by:  un12  4172  in12  4228  indif1  4281  difundi  4289  difundir  4290  difindi  4291  difindir  4292  dif32  4301  csbvarg  4433  undif1  4475  resmpt3  6055  xp0  6177  partfun  6714  fresaunres2  6779  caov12  7662  caov13  7664  caov411  7666  caovdir  7668  orduniss2  7854  fparlem3  8140  fparlem4  8141  fsplitfpar  8144  hartogslem1  9583  ttrclco  9759  kmlem3  10194  djuassen  10220  xpdjuen  10221  halfnq  11017  reclem3pr  11090  addcmpblnr  11110  ltsrpr  11118  pn0sr  11142  sqgt0sr  11147  map2psrpr  11151  negsubdii  11595  i4  14244  nn0opthlem1  14308  fac4  14321  imi  15197  bpoly3  16095  ef01bndlem  16221  bitsres  16511  gcdaddmlem  16562  modsubi  17111  gcdmodi  17113  numexpp1  17116  karatsuba  17122  oppgcntr  19385  frgpuplem  19791  0frgp  19798  pzriprnglem11  21503  ressmpladd  22048  ressmplmul  22049  ressmplvsca  22050  ltbwe  22063  ressply1add  22232  ressply1mul  22233  ressply1vsca  22234  sn0cld  23099  qtopres  23707  itg1addlem5  25736  cospi  26515  sincos4thpi  26556  sincos3rdpi  26560  dvlog  26694  dvlog2  26696  dvsqrt  26785  dvcnsqrt  26787  ang180lem3  26855  1cubrlem  26885  mcubic  26891  quart1lem  26899  atantayl2  26982  log2cnv  26988  log2ublem2  26991  log2ub  26993  gam1  27109  chtub  27257  bclbnd  27325  bposlem8  27336  lgsdir2lem1  27370  lgsdir2lem5  27374  2lgsoddprmlem3d  27458  ex-bc  30472  ex-gcd  30477  ipidsq  30730  ip1ilem  30846  ipdirilem  30849  ipasslem10  30859  siilem1  30871  hvmul2negi  31068  hvadd12i  31077  hvnegdii  31082  normlem1  31130  normlem9  31138  normsubi  31161  normpar2i  31176  polid2i  31177  chjassi  31506  chj12i  31542  pjoml2i  31605  hoadd12i  31797  lnophmlem2  32037  nmopcoadj2i  32122  indifundif  32544  aciunf1  32674  fressupp  32698  ffsrn  32741  dpmul10  32878  dpmul1000  32882  dpadd2  32893  dpadd  32894  dpmul  32896  cycpmconjslem1  33175  archirngz  33197  sqsscirc1  33908  sigaclfu2  34123  eulerpartlemd  34369  coinflippvt  34488  ballotth  34541  hgt750lem  34667  hgt750lem2  34668  quad3  35676  onint1  36451  bj-csbsn  36906  cnambfre  37676  sqmid3api  42323  redvmptabs  42395  re1m1e0m0  42432  sn-1ticom  42469  rabren3dioph  42831  arearect  43232  areaquad  43233  resnonrel  43610  cononrel1  43612  cononrel2  43613  lhe4.4ex1a  44353  expgrowthi  44357  expgrowth  44359  binomcxplemnotnn0  44380  liminf0  45813  dvcosre  45932  stoweidlem34  46054  fouriersw  46251  ceil5half3  47347  tposresg  48784  tposideq  48794