Theorem 3eqtr3i 2768

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

Syntax hints:   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  un12  4126  in12  4182  indif1  4235  difundi  4243  difundir  4244  difindi  4245  difindir  4246  dif32  4255  csbvarg  4387  undif1  4429  resmpt3  5998  xp0OLD  6117  partfun  6640  fresaunres2  6707  caov12  7588  caov13  7590  caov411  7592  caovdir  7594  orduniss2  7777  fparlem3  8058  fparlem4  8059  fsplitfpar  8062  hartogslem1  9451  ttrclco  9631  kmlem3  10067  djuassen  10093  xpdjuen  10094  halfnq  10891  reclem3pr  10964  addcmpblnr  10984  ltsrpr  10992  pn0sr  11016  sqgt0sr  11021  map2psrpr  11025  negsubdii  11470  i4  14131  nn0opthlem1  14195  fac4  14208  imi  15084  bpoly3  15985  ef01bndlem  16113  bitsres  16404  gcdaddmlem  16455  modsubi  17004  gcdmodi  17006  numexpp1  17009  karatsuba  17015  oppgcntr  19298  frgpuplem  19705  0frgp  19712  pzriprnglem11  21450  ressmpladd  21988  ressmplmul  21989  ressmplvsca  21990  ltbwe  22003  ressply1add  22174  ressply1mul  22175  ressply1vsca  22176  sn0cld  23038  qtopres  23646  itg1addlem5  25661  cospi  26441  sincos4thpi  26482  sincos3rdpi  26486  dvlog  26620  dvlog2  26622  dvsqrt  26711  dvcnsqrt  26713  ang180lem3  26781  1cubrlem  26811  mcubic  26817  quart1lem  26825  atantayl2  26908  log2cnv  26914  log2ublem2  26917  log2ub  26919  gam1  27035  chtub  27183  bclbnd  27251  bposlem8  27262  lgsdir2lem1  27296  lgsdir2lem5  27300  2lgsoddprmlem3d  27384  ex-bc  30531  ex-gcd  30536  ipidsq  30789  ip1ilem  30905  ipdirilem  30908  ipasslem10  30918  siilem1  30930  hvmul2negi  31127  hvadd12i  31136  hvnegdii  31141  normlem1  31189  normlem9  31197  normsubi  31220  normpar2i  31235  polid2i  31236  chjassi  31565  chj12i  31601  pjoml2i  31664  hoadd12i  31856  lnophmlem2  32096  nmopcoadj2i  32181  indifundif  32602  aciunf1  32744  partfun2  32757  fressupp  32769  ffsrn  32809  dpmul10  32978  dpmul1000  32982  dpadd2  32993  dpadd  32994  dpmul  32996  cycpmconjslem1  33238  archirngz  33273  psrbasfsupp  33695  cos9thpiminplylem4  33944  cos9thpiminplylem5  33945  sqsscirc1  34067  sigaclfu2  34280  eulerpartlemd  34525  coinflippvt  34644  ballotth  34697  hgt750lem  34810  hgt750lem2  34811  quad3  35866  onint1  36645  bj-csbsn  37107  cnambfre  37871  vxp  38466  sqmid3api  42605  sin2t3rdpi  42675  cos2t3rdpi  42676  sin4t3rdpi  42677  cos4t3rdpi  42678  redvmptabs  42682  re1m1e0m0  42719  sn-1ticom  42757  rabren3dioph  43124  arearect  43524  areaquad  43525  resnonrel  43900  cononrel1  43902  cononrel2  43903  lhe4.4ex1a  44637  expgrowthi  44641  expgrowth  44643  binomcxplemnotnn0  44664  liminf0  46104  dvcosre  46223  stoweidlem34  46345  fouriersw  46542  ceil5half3  47653  tposresg  49190  tposideq  49200