Theorem 3eqtr3i 2829

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

Syntax hints:   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  un12  4094  in12  4147  indif1  4198  difundi  4206  difundir  4207  difindi  4208  difindir  4209  dif32  4217  csbvarg  4339  undif1  4382  resmpt3  5873  xp0  5982  partfun  6467  fresaunres2  6524  caov12  7356  caov13  7358  caov411  7360  caovdir  7362  orduniss2  7528  fparlem3  7792  fparlem4  7793  fsplitfpar  7797  hartogslem1  8990  kmlem3  9563  djuassen  9589  xpdjuen  9590  halfnq  10387  reclem3pr  10460  addcmpblnr  10480  ltsrpr  10488  pn0sr  10512  sqgt0sr  10517  map2psrpr  10521  negsubdii  10960  halfpm6th  11846  i4  13563  nn0opthlem1  13624  fac4  13637  imi  14508  bpoly3  15404  ef01bndlem  15529  bitsres  15812  gcdaddmlem  15862  modsubi  16398  gcdmodi  16400  numexpp1  16404  karatsuba  16410  oppgcntr  18485  frgpuplem  18890  0frgp  18897  ressmpladd  20697  ressmplmul  20698  ressmplvsca  20699  ltbwe  20712  ressply1add  20859  ressply1mul  20860  ressply1vsca  20861  sn0cld  21695  qtopres  22303  itg1addlem5  24304  cospi  25065  sincos4thpi  25106  sincos3rdpi  25109  dvlog  25242  dvlog2  25244  dvsqrt  25331  dvcnsqrt  25333  ang180lem3  25397  1cubrlem  25427  mcubic  25433  quart1lem  25441  atantayl2  25524  log2cnv  25530  log2ublem2  25533  log2ub  25535  gam1  25650  chtub  25796  bclbnd  25864  bposlem8  25875  lgsdir2lem1  25909  lgsdir2lem5  25913  2lgsoddprmlem3d  25997  ex-bc  28237  ex-gcd  28242  ipidsq  28493  ip1ilem  28609  ipdirilem  28612  ipasslem10  28622  siilem1  28634  hvmul2negi  28831  hvadd12i  28840  hvnegdii  28845  normlem1  28893  normlem9  28901  normsubi  28924  normpar2i  28939  polid2i  28940  chjassi  29269  chj12i  29305  pjoml2i  29368  hoadd12i  29560  lnophmlem2  29800  nmopcoadj2i  29885  indifundif  30297  aciunf1  30426  fressupp  30448  ffsrn  30491  dpmul10  30597  dpmul1000  30601  dpadd2  30612  dpadd  30613  dpmul  30615  cycpmconjslem1  30846  archirngz  30868  sqsscirc1  31261  sigaclfu2  31490  eulerpartlemd  31734  coinflippvt  31852  ballotth  31905  hgt750lem  32032  hgt750lem2  32033  quad3  33026  onint1  33910  bj-csbsn  34345  cnambfre  35105  sqmid3api  39477  re1m1e0m0  39535  sn-1ticom  39571  rabren3dioph  39756  arearect  40165  areaquad  40166  resnonrel  40292  cononrel1  40294  cononrel2  40295  lhe4.4ex1a  41033  expgrowthi  41037  expgrowth  41039  binomcxplemnotnn0  41060  liminf0  42435  dvcosre  42554  stoweidlem34  42676  fouriersw  42873