Theorem 3eqtr3i 2760

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  un12  4136  in12  4192  indif1  4245  difundi  4253  difundir  4254  difindi  4255  difindir  4256  dif32  4265  csbvarg  4397  undif1  4439  resmpt3  6009  xp0  6131  partfun  6665  fresaunres2  6732  caov12  7617  caov13  7619  caov411  7621  caovdir  7623  orduniss2  7808  fparlem3  8093  fparlem4  8094  fsplitfpar  8097  hartogslem1  9495  ttrclco  9671  kmlem3  10106  djuassen  10132  xpdjuen  10133  halfnq  10929  reclem3pr  11002  addcmpblnr  11022  ltsrpr  11030  pn0sr  11054  sqgt0sr  11059  map2psrpr  11063  negsubdii  11507  i4  14169  nn0opthlem1  14233  fac4  14246  imi  15123  bpoly3  16024  ef01bndlem  16152  bitsres  16443  gcdaddmlem  16494  modsubi  17043  gcdmodi  17045  numexpp1  17048  karatsuba  17054  oppgcntr  19297  frgpuplem  19702  0frgp  19709  pzriprnglem11  21401  ressmpladd  21936  ressmplmul  21937  ressmplvsca  21938  ltbwe  21951  ressply1add  22114  ressply1mul  22115  ressply1vsca  22116  sn0cld  22977  qtopres  23585  itg1addlem5  25601  cospi  26381  sincos4thpi  26422  sincos3rdpi  26426  dvlog  26560  dvlog2  26562  dvsqrt  26651  dvcnsqrt  26653  ang180lem3  26721  1cubrlem  26751  mcubic  26757  quart1lem  26765  atantayl2  26848  log2cnv  26854  log2ublem2  26857  log2ub  26859  gam1  26975  chtub  27123  bclbnd  27191  bposlem8  27202  lgsdir2lem1  27236  lgsdir2lem5  27240  2lgsoddprmlem3d  27324  ex-bc  30381  ex-gcd  30386  ipidsq  30639  ip1ilem  30755  ipdirilem  30758  ipasslem10  30768  siilem1  30780  hvmul2negi  30977  hvadd12i  30986  hvnegdii  30991  normlem1  31039  normlem9  31047  normsubi  31070  normpar2i  31085  polid2i  31086  chjassi  31415  chj12i  31451  pjoml2i  31514  hoadd12i  31706  lnophmlem2  31946  nmopcoadj2i  32031  indifundif  32453  aciunf1  32587  fressupp  32611  ffsrn  32652  dpmul10  32815  dpmul1000  32819  dpadd2  32830  dpadd  32831  dpmul  32833  cycpmconjslem1  33111  archirngz  33143  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  sqsscirc1  33898  sigaclfu2  34111  eulerpartlemd  34357  coinflippvt  34476  ballotth  34529  hgt750lem  34642  hgt750lem2  34643  quad3  35657  onint1  36437  bj-csbsn  36892  cnambfre  37662  sqmid3api  42271  sin2t3rdpi  42341  cos2t3rdpi  42342  sin4t3rdpi  42343  cos4t3rdpi  42344  redvmptabs  42348  re1m1e0m0  42385  sn-1ticom  42423  rabren3dioph  42803  arearect  43204  areaquad  43205  resnonrel  43581  cononrel1  43583  cononrel2  43584  lhe4.4ex1a  44318  expgrowthi  44322  expgrowth  44324  binomcxplemnotnn0  44345  liminf0  45791  dvcosre  45910  stoweidlem34  46032  fouriersw  46229  ceil5half3  47338  tposresg  48863  tposideq  48873