Theorem 3eqtr3i 2794

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

This proof depends on syntax axioms:   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755

This theorem is used by:  in12  4128  un12  4174  indif1  4230  difundi  4238  difundir  4239  difindi  4240  difindir  4241  dif32  4250  csbvarg  4395  undif1  4433  unidif0  5325  resmpt3  6036  xp0OLD  6155  partfun  6697  fresaunres2  6765  caov12  7659  caov13  7661  caov411  7663  caovdir  7665  orduniss2  7854  fparlem3  8138  fparlem4  8139  fsplitfpar  8142  hartogslem1  9549  ttrclco  9732  kmlem3  10244  djuassen  10270  xpdjuen  10271  halfnq  11074  reclem3pr  11147  addcmpblnr  11167  ltsrpr  11175  pn0sr  11199  sqgt0sr  11204  map2psrpr  11208  negsubdii  11656  8th4div3  12579  i4  14361  nn0opthlem1  14425  fac4  14438  imi  15339  bpoly3  16239  ef01bndlem  16367  bitsres  16658  gcdaddmlem  16711  modsubi  17265  gcdmodi  17267  numexpp1  17270  karatsuba  17276  oppgcntr  19594  frgpuplem  20001  0frgp  20008  pzriprnglem11  21812  ressmpladd  22352  ressmplmul  22353  ressmplvsca  22354  ltbwe  22368  ressply1add  22562  ressply1mul  22563  ressply1vsca  22564  sn0cld  23423  qtopres  24032  itg1addlem5  26036  cospi  26816  sincos4thpi  26857  sincos3rdpi  26860  dvlog  26994  dvlog2  26996  dvsqrt  27085  dvcnsqrt  27087  ang180lem3  27154  1cubrlem  27184  mcubic  27190  quart1lem  27198  atantayl2  27281  log2cnv  27287  log2ublem2  27290  log2ub  27292  gam1  27407  chtub  27554  bclbnd  27622  bposlem8  27633  lgsdir2lem1  27667  lgsdir2lem5  27671  2lgsoddprmlem3d  27755  ex-bc  31068  ex-gcd  31073  ipidsq  31327  ip1ilem  31443  ipdirilem  31446  ipasslem10  31456  siilem1  31468  hvmul2negi  31665  hvadd12i  31674  hvnegdii  31679  normlem1  31727  normlem9  31735  normsubi  31758  normpar2i  31773  polid2i  31774  chjassi  32103  chj12i  32139  pjoml2i  32202  hoadd12i  32394  lnophmlem2  32634  nmopcoadj2i  32719  indifundif  33177  ififcom  33203  aciunf1  33314  partfun2  33327  fressupp  33338  ffsrn  33376  dpmul10  33517  dpmul1000  33521  dpadd2  33532  dpadd  33533  dpmul  33535  cycpmconjslem1  33771  archirngz  33806  psrbasfsupp  34199  cos9thpiminplylem4  34473  cos9thpiminplylem5  34474  sqsscirc1  34596  sigaclfu2  34809  eulerpartlemd  35054  coinflippvt  35173  ballotth  35226  hgt750lem  35336  hgt750lem2  35337  quad3  36559  onint1  37370  bj-csbsn  37949  cnambfre  38732  vxp  39341  sqmid3api  43486  sin2t3rdpi  43550  cos2t3rdpi  43551  sin4t3rdpi  43552  cos4t3rdpi  43553  redvmptabs  43557  re1m1e0m0  43594  sn-1ticom  43632  rabren3dioph  43968  arearect  44363  areaquad  44364  resnonrel  44738  cononrel1  44740  cononrel2  44741  lhe4.4ex1a  45459  expgrowthi  45463  expgrowth  45465  binomcxplemnotnn0  45486  liminf0  46948  dvcosre  47067  stoweidlem34  47189  fouriersw  47386  goldratmolem2  48078  ceil5half3  48561  tposresg  50136  tposideq  50146  veroquadgsumlem  51203