Theorem 3eqtr3i 2652

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	|- A = B
3eqtr3i.2	|- A = C
3eqtr3i.3	|- B = D

Assertion

Ref	Expression
3eqtr3i	|- C = D

Proof of Theorem 3eqtr3i

Step	Hyp	Ref	Expression
1		3eqtr3i.1	. . 3 |- A = B
2		3eqtr3i.2	. . 3 |- A = C
3	1, 2	eqtr3i 2646	. 2 |- B = C
4		3eqtr3i.3	. 2 |- B = D
5	3, 4	eqtr3i 2646	1 |- C = D

Syntax hints:   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  un12  3771  in12  3824  indif1  3871  difundi  3879  difundir  3880  difindi  3881  difindir  3882  dif32  3891  csbvarg  4003  undif1  4043  resmpt3  5450  xp0  5552  fresaunres2  6076  fvsnun1  6448  caov12  6862  caov13  6864  caov411  6866  caovdir  6868  orduniss2  7033  fparlem3  7279  fparlem4  7280  hartogslem1  8447  kmlem3  8974  cdaassen  9004  xpcdaen  9005  halfnq  9798  reclem3pr  9871  addcmpblnr  9890  ltsrpr  9898  pn0sr  9922  sqgt0sr  9927  map2psrpr  9931  negsubdii  10366  halfpm6th  11253  decmul1  11585  i4  12967  nn0opthlem1  13055  fac4  13068  imi  13897  bpoly3  14789  ef01bndlem  14914  bitsres  15195  gcdaddmlem  15245  modsubi  15776  gcdmodi  15778  numexpp1  15782  karatsuba  15792  karatsubaOLD  15793  oppgcntr  17795  frgpuplem  18185  ressmpladd  19457  ressmplmul  19458  ressmplvsca  19459  ltbwe  19472  ressply1add  19600  ressply1mul  19601  ressply1vsca  19602  sn0cld  20894  qtopres  21501  itg1addlem5  23467  cospi  24224  sincos4thpi  24265  sincos3rdpi  24268  dvlog  24397  dvlog2  24399  dvsqrt  24483  dvcnsqrt  24485  ang180lem3  24541  1cubrlem  24568  mcubic  24574  quart1lem  24582  atantayl2  24665  log2cnv  24671  log2ublem2  24674  log2ub  24676  gam1  24791  chtub  24937  bclbnd  25005  bposlem8  25016  lgsdir2lem1  25050  lgsdir2lem5  25054  2lgsoddprmlem3d  25138  ex-bc  27309  ex-gcd  27314  ipidsq  27565  ip1ilem  27681  ipdirilem  27684  ipasslem10  27694  siilem1  27706  hvmul2negi  27905  hvadd12i  27914  hvnegdii  27919  normlem1  27967  normlem9  27975  normsubi  27998  normpar2i  28013  polid2i  28014  chjassi  28345  chj12i  28381  pjoml2i  28444  hoadd12i  28636  lnophmlem2  28876  nmopcoadj2i  28961  indifundif  29356  aciunf1  29463  partfun  29475  ffsrn  29504  dpmul10  29603  dpmul1000  29607  dpadd2  29618  dpadd  29619  dpmul  29621  archirngz  29743  sqsscirc1  29954  sigaclfu2  30184  eulerpartlemd  30428  coinflippvt  30546  ballotth  30599  hgt750lem  30729  hgt750lem2  30730  quad3  31564  onint1  32448  bj-csbsn  32899  cnambfre  33458  rabren3dioph  37379  arearect  37801  areaquad  37802  resnonrel  37898  cononrel1  37900  cononrel2  37901  lhe4.4ex1a  38528  expgrowthi  38532  expgrowth  38534  binomcxplemnotnn0  38555  liminf0  40025  dvcosre  40126  stoweidlem34  40251  fouriersw  40448