Theorem 3eqtr3i 2640

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

Syntax hints:   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  un12  3733  in12  3786  indif1  3830  difundi  3838  difundir  3839  difindi  3840  difindir  3841  dif32  3850  csbvarg  3955  undif1  3995  resmpt3  5370  xp0  5471  fresaunres2  5989  fvsnun1  6353  caov12  6760  caov13  6762  caov411  6764  caovdir  6766  orduniss2  6925  fparlem3  7166  fparlem4  7167  hartogslem1  8330  kmlem3  8857  cdaassen  8887  xpcdaen  8888  halfnq  9677  reclem3pr  9750  addcmpblnr  9769  ltsrpr  9777  pn0sr  9801  sqgt0sr  9806  map2psrpr  9810  negsubdii  10245  halfpm6th  11130  decmul1  11461  i4  12829  nn0opthlem1  12917  fac4  12930  imi  13745  bpoly3  14628  ef01bndlem  14753  bitsres  15033  gcdaddmlem  15083  modsubi  15614  gcdmodi  15616  numexpp1  15620  karatsuba  15630  karatsubaOLD  15631  oppgcntr  17618  frgpuplem  18008  ressmpladd  19278  ressmplmul  19279  ressmplvsca  19280  ltbwe  19293  ressply1add  19421  ressply1mul  19422  ressply1vsca  19423  sn0cld  20704  qtopres  21311  itg1addlem5  23273  cospi  24028  sincos4thpi  24069  sincos3rdpi  24072  dvlog  24197  dvlog2  24199  dvsqrt  24283  dvcnsqrt  24285  ang180lem3  24341  1cubrlem  24368  mcubic  24374  quart1lem  24382  atantayl2  24465  log2cnv  24471  log2ublem2  24474  log2ub  24476  gam1  24591  chtub  24737  bclbnd  24805  bposlem8  24816  lgsdir2lem1  24850  lgsdir2lem5  24854  2lgsoddprmlem3d  24938  ex-bc  26701  ex-gcd  26706  ipidsq  26949  ip1ilem  27065  ipdirilem  27068  ipasslem10  27078  siilem1  27090  hvmul2negi  27289  hvadd12i  27298  hvnegdii  27303  normlem1  27351  normlem9  27359  normsubi  27382  normpar2i  27397  polid2i  27398  chjassi  27729  chj12i  27765  pjoml2i  27828  hoadd12i  28020  lnophmlem2  28260  nmopcoadj2i  28345  indifundif  28740  aciunf1  28845  partfun  28858  ffsrn  28892  archirngz  29074  sqsscirc1  29282  sigaclfu2  29511  eulerpartlemd  29755  coinflippvt  29873  ballotth  29926  quad3  30818  onint1  31618  bj-csbsn  32091  cnambfre  32628  rabren3dioph  36397  arearect  36820  areaquad  36821  resnonrel  36917  cononrel1  36919  cononrel2  36920  lhe4.4ex1a  37550  expgrowthi  37554  expgrowth  37556  binomcxplemnotnn0  37577  dvcosre  38799  stoweidlem34  38927  fouriersw  39124