Theorem 3eqtr3i 2767

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

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

This theorem is referenced by:  un12  4153  in12  4209  indif1  4262  difundi  4270  difundir  4271  difindi  4272  difindir  4273  dif32  4282  csbvarg  4414  undif1  4456  resmpt3  6030  xp0  6152  partfun  6690  fresaunres2  6755  caov12  7640  caov13  7642  caov411  7644  caovdir  7646  orduniss2  7832  fparlem3  8118  fparlem4  8119  fsplitfpar  8122  hartogslem1  9561  ttrclco  9737  kmlem3  10172  djuassen  10198  xpdjuen  10199  halfnq  10995  reclem3pr  11068  addcmpblnr  11088  ltsrpr  11096  pn0sr  11120  sqgt0sr  11125  map2psrpr  11129  negsubdii  11573  i4  14227  nn0opthlem1  14291  fac4  14304  imi  15181  bpoly3  16079  ef01bndlem  16207  bitsres  16497  gcdaddmlem  16548  modsubi  17097  gcdmodi  17099  numexpp1  17102  karatsuba  17108  oppgcntr  19353  frgpuplem  19758  0frgp  19765  pzriprnglem11  21457  ressmpladd  21992  ressmplmul  21993  ressmplvsca  21994  ltbwe  22007  ressply1add  22170  ressply1mul  22171  ressply1vsca  22172  sn0cld  23033  qtopres  23641  itg1addlem5  25658  cospi  26438  sincos4thpi  26479  sincos3rdpi  26483  dvlog  26617  dvlog2  26619  dvsqrt  26708  dvcnsqrt  26710  ang180lem3  26778  1cubrlem  26808  mcubic  26814  quart1lem  26822  atantayl2  26905  log2cnv  26911  log2ublem2  26914  log2ub  26916  gam1  27032  chtub  27180  bclbnd  27248  bposlem8  27259  lgsdir2lem1  27293  lgsdir2lem5  27297  2lgsoddprmlem3d  27381  ex-bc  30438  ex-gcd  30443  ipidsq  30696  ip1ilem  30812  ipdirilem  30815  ipasslem10  30825  siilem1  30837  hvmul2negi  31034  hvadd12i  31043  hvnegdii  31048  normlem1  31096  normlem9  31104  normsubi  31127  normpar2i  31142  polid2i  31143  chjassi  31472  chj12i  31508  pjoml2i  31571  hoadd12i  31763  lnophmlem2  32003  nmopcoadj2i  32088  indifundif  32510  aciunf1  32646  fressupp  32670  ffsrn  32711  dpmul10  32874  dpmul1000  32878  dpadd2  32889  dpadd  32890  dpmul  32892  cycpmconjslem1  33170  archirngz  33192  cos9thpiminplylem4  33824  cos9thpiminplylem5  33825  sqsscirc1  33944  sigaclfu2  34157  eulerpartlemd  34403  coinflippvt  34522  ballotth  34575  hgt750lem  34688  hgt750lem2  34689  quad3  35697  onint1  36472  bj-csbsn  36927  cnambfre  37697  sqmid3api  42300  redvmptabs  42370  re1m1e0m0  42407  sn-1ticom  42444  rabren3dioph  42805  arearect  43206  areaquad  43207  resnonrel  43583  cononrel1  43585  cononrel2  43586  lhe4.4ex1a  44320  expgrowthi  44324  expgrowth  44326  binomcxplemnotnn0  44347  liminf0  45789  dvcosre  45908  stoweidlem34  46030  fouriersw  46227  ceil5half3  47336  tposresg  48820  tposideq  48830