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 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is used by:  un12  4126  in12  4181  indif1  4235  difundi  4243  difundir  4244  difindi  4245  difindir  4246  dif32  4255  csbvarg  4399  undif1  4437  unidif0  5330  resmpt3  6040  xp0OLD  6155  partfun  6682  fresaunres2  6750  caov12  7638  caov13  7640  caov411  7642  caovdir  7644  orduniss2  7825  fparlem3  8105  fparlem4  8106  fsplitfpar  8109  hartogslem1  9500  ttrclco  9683  kmlem3  10141  djuassen  10167  xpdjuen  10168  halfnq  10965  reclem3pr  11038  addcmpblnr  11058  ltsrpr  11066  pn0sr  11090  sqgt0sr  11095  map2psrpr  11099  negsubdii  11547  8th4div3  12468  i4  14245  nn0opthlem1  14309  fac4  14322  imi  15213  bpoly3  16116  ef01bndlem  16244  bitsres  16535  gcdaddmlem  16586  modsubi  17136  gcdmodi  17138  numexpp1  17141  karatsuba  17147  oppgcntr  19439  frgpuplem  19846  0frgp  19853  pzriprnglem11  21650  ressmpladd  22188  ressmplmul  22189  ressmplvsca  22190  ltbwe  22204  ressply1add  22398  ressply1mul  22399  ressply1vsca  22400  sn0cld  23256  qtopres  23864  itg1addlem5  25868  cospi  26646  sincos4thpi  26687  sincos3rdpi  26691  dvlog  26825  dvlog2  26827  dvsqrt  26916  dvcnsqrt  26918  ang180lem3  26985  1cubrlem  27015  mcubic  27021  quart1lem  27029  atantayl2  27112  log2cnv  27118  log2ublem2  27121  log2ub  27123  gam1  27238  chtub  27385  bclbnd  27453  bposlem8  27464  lgsdir2lem1  27498  lgsdir2lem5  27502  2lgsoddprmlem3d  27586  ex-bc  30812  ex-gcd  30817  ipidsq  31071  ip1ilem  31187  ipdirilem  31190  ipasslem10  31200  siilem1  31212  hvmul2negi  31409  hvadd12i  31418  hvnegdii  31423  normlem1  31471  normlem9  31479  normsubi  31502  normpar2i  31517  polid2i  31518  chjassi  31847  chj12i  31883  pjoml2i  31946  hoadd12i  32138  lnophmlem2  32378  nmopcoadj2i  32463  indifundif  32879  ififcom  32905  aciunf1  33017  partfun2  33030  fressupp  33042  ffsrn  33082  dpmul10  33223  dpmul1000  33227  dpadd2  33238  dpadd  33239  dpmul  33241  cycpmconjslem1  33483  archirngz  33518  psrbasfsupp  33910  cos9thpiminplylem4  34184  cos9thpiminplylem5  34185  sqsscirc1  34307  sigaclfu2  34520  eulerpartlemd  34765  coinflippvt  34884  ballotth  34937  hgt750lem  35047  hgt750lem2  35048  quad3  36170  onint1  36988  bj-csbsn  37567  cnambfre  38347  vxp  38940  sqmid3api  43072  sin2t3rdpi  43142  cos2t3rdpi  43143  sin4t3rdpi  43144  cos4t3rdpi  43145  redvmptabs  43149  re1m1e0m0  43186  sn-1ticom  43224  rabren3dioph  43570  arearect  43970  areaquad  43971  resnonrel  44346  cononrel1  44348  cononrel2  44349  lhe4.4ex1a  45067  expgrowthi  45071  expgrowth  45073  binomcxplemnotnn0  45094  liminf0  46535  dvcosre  46654  stoweidlem34  46776  fouriersw  46973  goldratmolem2  47651  ceil5half3  48111  tposresg  49684  tposideq  49694