Theorem 3eqtr3i 2810

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

Syntax hints:   = wceq 1507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2771

This theorem is referenced by:  un12  4034  in12  4086  indif1  4137  difundi  4145  difundir  4146  difindi  4147  difindir  4148  dif32  4156  csbvarg  4268  undif1  4308  resmpt3  5753  xp0  5857  fresaunres2  6381  fvsnun1OLD  6773  caov12  7194  caov13  7196  caov411  7198  caovdir  7200  orduniss2  7366  fparlem3  7619  fparlem4  7620  hartogslem1  8803  kmlem3  9374  djuassen  9404  xpdjuen  9405  halfnq  10198  reclem3pr  10271  addcmpblnr  10291  ltsrpr  10299  pn0sr  10323  sqgt0sr  10328  map2psrpr  10332  negsubdii  10774  halfpm6th  11671  decmul1OLD  11980  i4  13385  nn0opthlem1  13446  fac4  13459  imi  14380  bpoly3  15275  ef01bndlem  15400  bitsres  15685  gcdaddmlem  15735  modsubi  16267  gcdmodi  16269  numexpp1  16273  karatsuba  16279  oppgcntr  18267  frgpuplem  18661  ressmpladd  19954  ressmplmul  19955  ressmplvsca  19956  ltbwe  19969  ressply1add  20104  ressply1mul  20105  ressply1vsca  20106  sn0cld  21405  qtopres  22013  itg1addlem5  24007  cospi  24764  sincos4thpi  24805  sincos3rdpi  24808  dvlog  24938  dvlog2  24940  dvsqrt  25027  dvcnsqrt  25029  ang180lem3  25093  1cubrlem  25123  mcubic  25129  quart1lem  25137  atantayl2  25220  log2cnv  25227  log2ublem2  25230  log2ub  25232  gam1  25347  chtub  25493  bclbnd  25561  bposlem8  25572  lgsdir2lem1  25606  lgsdir2lem5  25610  2lgsoddprmlem3d  25694  ex-bc  28012  ex-gcd  28017  ipidsq  28267  ip1ilem  28383  ipdirilem  28386  ipasslem10  28396  siilem1  28408  hvmul2negi  28607  hvadd12i  28616  hvnegdii  28621  normlem1  28669  normlem9  28677  normsubi  28700  normpar2i  28715  polid2i  28716  chjassi  29047  chj12i  29083  pjoml2i  29146  hoadd12i  29338  lnophmlem2  29578  nmopcoadj2i  29663  indifundif  30062  aciunf1  30173  partfun  30186  ffsrn  30220  dpmul10  30320  dpmul1000  30324  dpadd2  30335  dpadd  30336  dpmul  30338  archirngz  30484  sqsscirc1  30795  sigaclfu2  31025  eulerpartlemd  31269  coinflippvt  31388  ballotth  31441  hgt750lem  31570  hgt750lem2  31571  quad3  32433  onint1  33317  bj-csbsn  33713  cnambfre  34381  sqmid3api  38601  rabren3dioph  38808  arearect  39218  areaquad  39219  resnonrel  39314  cononrel1  39316  cononrel2  39317  lhe4.4ex1a  40077  expgrowthi  40081  expgrowth  40083  binomcxplemnotnn0  40104  liminf0  41506  dvcosre  41627  stoweidlem34  41751  fouriersw  41948