Theorem 3eqtr3i 2771

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

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  un12  4183  in12  4237  indif1  4288  difundi  4296  difundir  4297  difindi  4298  difindir  4299  dif32  4308  csbvarg  4440  undif1  4482  resmpt3  6058  xp0  6180  partfun  6716  fresaunres2  6781  caov12  7661  caov13  7663  caov411  7665  caovdir  7667  orduniss2  7853  fparlem3  8138  fparlem4  8139  fsplitfpar  8142  hartogslem1  9580  ttrclco  9756  kmlem3  10191  djuassen  10217  xpdjuen  10218  halfnq  11014  reclem3pr  11087  addcmpblnr  11107  ltsrpr  11115  pn0sr  11139  sqgt0sr  11144  map2psrpr  11148  negsubdii  11592  halfpm6th  12485  i4  14240  nn0opthlem1  14304  fac4  14317  imi  15193  bpoly3  16091  ef01bndlem  16217  bitsres  16507  gcdaddmlem  16558  modsubi  17106  gcdmodi  17108  numexpp1  17112  karatsuba  17118  oppgcntr  19399  frgpuplem  19805  0frgp  19812  pzriprnglem11  21520  ressmpladd  22065  ressmplmul  22066  ressmplvsca  22067  ltbwe  22080  ressply1add  22247  ressply1mul  22248  ressply1vsca  22249  sn0cld  23114  qtopres  23722  itg1addlem5  25750  cospi  26529  sincos4thpi  26570  sincos3rdpi  26574  dvlog  26708  dvlog2  26710  dvsqrt  26799  dvcnsqrt  26801  ang180lem3  26869  1cubrlem  26899  mcubic  26905  quart1lem  26913  atantayl2  26996  log2cnv  27002  log2ublem2  27005  log2ub  27007  gam1  27123  chtub  27271  bclbnd  27339  bposlem8  27350  lgsdir2lem1  27384  lgsdir2lem5  27388  2lgsoddprmlem3d  27472  ex-bc  30481  ex-gcd  30486  ipidsq  30739  ip1ilem  30855  ipdirilem  30858  ipasslem10  30868  siilem1  30880  hvmul2negi  31077  hvadd12i  31086  hvnegdii  31091  normlem1  31139  normlem9  31147  normsubi  31170  normpar2i  31185  polid2i  31186  chjassi  31515  chj12i  31551  pjoml2i  31614  hoadd12i  31806  lnophmlem2  32046  nmopcoadj2i  32131  indifundif  32552  aciunf1  32680  fressupp  32703  ffsrn  32747  dpmul10  32862  dpmul1000  32866  dpadd2  32877  dpadd  32878  dpmul  32880  cycpmconjslem1  33157  archirngz  33179  sqsscirc1  33869  sigaclfu2  34102  eulerpartlemd  34348  coinflippvt  34466  ballotth  34519  hgt750lem  34645  hgt750lem2  34646  quad3  35655  onint1  36432  bj-csbsn  36887  cnambfre  37655  sqmid3api  42297  redvmptabs  42369  re1m1e0m0  42404  sn-1ticom  42441  rabren3dioph  42803  arearect  43204  areaquad  43205  resnonrel  43582  cononrel1  43584  cononrel2  43585  lhe4.4ex1a  44325  expgrowthi  44329  expgrowth  44331  binomcxplemnotnn0  44352  liminf0  45749  dvcosre  45868  stoweidlem34  45990  fouriersw  46187  ceil5half3  47280