Theorem 3eqtr3i 2764

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

Syntax hints:   = wceq 1534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720

This theorem is referenced by:  un12  4167  in12  4221  indif1  4272  difundi  4280  difundir  4281  difindi  4282  difindir  4283  dif32  4293  csbvarg  4432  undif1  4476  resmpt3  6042  xp0  6162  partfun  6702  fresaunres2  6769  caov12  7649  caov13  7651  caov411  7653  caovdir  7655  orduniss2  7836  fparlem3  8119  fparlem4  8120  fsplitfpar  8123  hartogslem1  9565  ttrclco  9741  kmlem3  10175  djuassen  10201  xpdjuen  10202  halfnq  10999  reclem3pr  11072  addcmpblnr  11092  ltsrpr  11100  pn0sr  11124  sqgt0sr  11129  map2psrpr  11133  negsubdii  11575  halfpm6th  12463  i4  14199  nn0opthlem1  14259  fac4  14272  imi  15136  bpoly3  16034  ef01bndlem  16160  bitsres  16447  gcdaddmlem  16498  modsubi  17040  gcdmodi  17042  numexpp1  17046  karatsuba  17052  oppgcntr  19318  frgpuplem  19726  0frgp  19733  pzriprnglem11  21416  ressmpladd  21966  ressmplmul  21967  ressmplvsca  21968  ltbwe  21981  ressply1add  22147  ressply1mul  22148  ressply1vsca  22149  sn0cld  22993  qtopres  23601  itg1addlem5  25629  cospi  26406  sincos4thpi  26447  sincos3rdpi  26450  dvlog  26584  dvlog2  26586  dvsqrt  26675  dvcnsqrt  26677  ang180lem3  26742  1cubrlem  26772  mcubic  26778  quart1lem  26786  atantayl2  26869  log2cnv  26875  log2ublem2  26878  log2ub  26880  gam1  26996  chtub  27144  bclbnd  27212  bposlem8  27223  lgsdir2lem1  27257  lgsdir2lem5  27261  2lgsoddprmlem3d  27345  ex-bc  30261  ex-gcd  30266  ipidsq  30519  ip1ilem  30635  ipdirilem  30638  ipasslem10  30648  siilem1  30660  hvmul2negi  30857  hvadd12i  30866  hvnegdii  30871  normlem1  30919  normlem9  30927  normsubi  30950  normpar2i  30965  polid2i  30966  chjassi  31295  chj12i  31331  pjoml2i  31394  hoadd12i  31586  lnophmlem2  31826  nmopcoadj2i  31911  indifundif  32320  aciunf1  32448  fressupp  32468  ffsrn  32511  dpmul10  32618  dpmul1000  32622  dpadd2  32633  dpadd  32634  dpmul  32636  cycpmconjslem1  32875  archirngz  32897  sqsscirc1  33509  sigaclfu2  33740  eulerpartlemd  33986  coinflippvt  34104  ballotth  34157  hgt750lem  34283  hgt750lem2  34284  quad3  35274  onint1  35933  bj-csbsn  36382  cnambfre  37141  sqmid3api  41857  re1m1e0m0  41952  sn-1ticom  41989  rabren3dioph  42235  arearect  42643  areaquad  42644  resnonrel  43022  cononrel1  43024  cononrel2  43025  lhe4.4ex1a  43766  expgrowthi  43770  expgrowth  43772  binomcxplemnotnn0  43793  liminf0  45181  dvcosre  45300  stoweidlem34  45422  fouriersw  45619

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »