Theorem 3eqtr3i 2795

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

Syntax hints:   = wceq 1562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756

This theorem is referenced by:  un12  4127  in12  4182  indif1  4236  difundi  4244  difundir  4245  difindi  4246  difindir  4247  dif32  4256  csbvarg  4390  undif1  4432  unidif0  5318  resmpt3  6029  xp0OLD  6145  partfun  6670  fresaunres2  6738  caov12  7626  caov13  7628  caov411  7630  caovdir  7632  orduniss2  7815  fparlem3  8095  fparlem4  8096  fsplitfpar  8099  hartogslem1  9492  ttrclco  9675  kmlem3  10111  djuassen  10137  xpdjuen  10138  halfnq  10936  reclem3pr  11009  addcmpblnr  11029  ltsrpr  11037  pn0sr  11061  sqgt0sr  11066  map2psrpr  11070  negsubdii  11518  i4  14219  nn0opthlem1  14283  fac4  14296  imi  15186  bpoly3  16090  ef01bndlem  16218  bitsres  16509  gcdaddmlem  16560  modsubi  17110  gcdmodi  17112  numexpp1  17115  karatsuba  17121  oppgcntr  19407  frgpuplem  19814  0frgp  19821  pzriprnglem11  21545  ressmpladd  22083  ressmplmul  22084  ressmplvsca  22085  ltbwe  22099  ressply1add  22293  ressply1mul  22294  ressply1vsca  22295  sn0cld  23152  qtopres  23760  itg1addlem5  25764  cospi  26539  sincos4thpi  26580  sincos3rdpi  26584  dvlog  26718  dvlog2  26720  dvsqrt  26809  dvcnsqrt  26811  ang180lem3  26878  1cubrlem  26908  mcubic  26914  quart1lem  26922  atantayl2  27005  log2cnv  27011  log2ublem2  27014  log2ub  27016  gam1  27131  chtub  27278  bclbnd  27346  bposlem8  27357  lgsdir2lem1  27391  lgsdir2lem5  27395  2lgsoddprmlem3d  27479  ex-bc  30656  ex-gcd  30661  ipidsq  30915  ip1ilem  31031  ipdirilem  31034  ipasslem10  31044  siilem1  31056  hvmul2negi  31253  hvadd12i  31262  hvnegdii  31267  normlem1  31315  normlem9  31323  normsubi  31346  normpar2i  31361  polid2i  31362  chjassi  31691  chj12i  31727  pjoml2i  31790  hoadd12i  31982  lnophmlem2  32222  nmopcoadj2i  32307  indifundif  32725  ififcom  32751  aciunf1  32867  partfun2  32880  fressupp  32892  ffsrn  32932  dpmul10  33074  dpmul1000  33078  dpadd2  33089  dpadd  33090  dpmul  33092  cycpmconjslem1  33336  archirngz  33371  psrbasfsupp  33810  cos9thpiminplylem4  34084  cos9thpiminplylem5  34085  sqsscirc1  34207  sigaclfu2  34420  eulerpartlemd  34665  coinflippvt  34784  ballotth  34837  hgt750lem  34947  hgt750lem2  34948  quad3  36025  onint1  36814  bj-csbsn  37394  cnambfre  38172  vxp  38767  sqmid3api  42897  sin2t3rdpi  42967  cos2t3rdpi  42968  sin4t3rdpi  42969  cos4t3rdpi  42970  redvmptabs  42974  re1m1e0m0  43011  sn-1ticom  43049  rabren3dioph  43397  arearect  43797  areaquad  43798  resnonrel  44173  cononrel1  44175  cononrel2  44176  lhe4.4ex1a  44910  expgrowthi  44914  expgrowth  44916  binomcxplemnotnn0  44937  liminf0  46372  dvcosre  46491  stoweidlem34  46613  fouriersw  46810  goldratmolem2  47485  ceil5half3  47945  tposresg  49504  tposideq  49514