MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr3i Structured version   Visualization version   GIF version

Theorem 3eqtr3i 2855
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
StepHypRef Expression
1 3eqtr3i.1 . . 3 𝐴 = 𝐵
2 3eqtr3i.2 . . 3 𝐴 = 𝐶
31, 2eqtr3i 2849 . 2 𝐵 = 𝐶
4 3eqtr3i.3 . 2 𝐵 = 𝐷
53, 4eqtr3i 2849 1 𝐶 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817
This theorem is referenced by:  un12  4129  in12  4182  indif1  4233  difundi  4241  difundir  4242  difindi  4243  difindir  4244  dif32  4252  csbvarg  4366  undif1  4407  resmpt3  5893  xp0  6002  fresaunres2  6540  caov12  7370  caov13  7372  caov411  7374  caovdir  7376  orduniss2  7542  fparlem3  7805  fparlem4  7806  fsplitfpar  7810  hartogslem1  9003  kmlem3  9576  djuassen  9602  xpdjuen  9603  halfnq  10396  reclem3pr  10469  addcmpblnr  10489  ltsrpr  10497  pn0sr  10521  sqgt0sr  10526  map2psrpr  10530  negsubdii  10969  halfpm6th  11855  i4  13572  nn0opthlem1  13633  fac4  13646  imi  14516  bpoly3  15412  ef01bndlem  15537  bitsres  15820  gcdaddmlem  15870  modsubi  16406  gcdmodi  16408  numexpp1  16412  karatsuba  16418  oppgcntr  18493  frgpuplem  18898  0frgp  18905  ressmpladd  20704  ressmplmul  20705  ressmplvsca  20706  ltbwe  20719  ressply1add  20866  ressply1mul  20867  ressply1vsca  20868  sn0cld  21701  qtopres  22309  itg1addlem5  24310  cospi  25071  sincos4thpi  25112  sincos3rdpi  25115  dvlog  25248  dvlog2  25250  dvsqrt  25337  dvcnsqrt  25339  ang180lem3  25403  1cubrlem  25433  mcubic  25439  quart1lem  25447  atantayl2  25530  log2cnv  25536  log2ublem2  25539  log2ub  25541  gam1  25656  chtub  25802  bclbnd  25870  bposlem8  25881  lgsdir2lem1  25915  lgsdir2lem5  25919  2lgsoddprmlem3d  26003  ex-bc  28243  ex-gcd  28248  ipidsq  28499  ip1ilem  28615  ipdirilem  28618  ipasslem10  28628  siilem1  28640  hvmul2negi  28837  hvadd12i  28846  hvnegdii  28851  normlem1  28899  normlem9  28907  normsubi  28930  normpar2i  28945  polid2i  28946  chjassi  29275  chj12i  29311  pjoml2i  29374  hoadd12i  29566  lnophmlem2  29806  nmopcoadj2i  29891  indifundif  30299  aciunf1  30422  partfun  30435  ffsrn  30479  dpmul10  30585  dpmul1000  30589  dpadd2  30600  dpadd  30601  dpmul  30603  cycpmconjslem1  30831  archirngz  30853  sqsscirc1  31211  sigaclfu2  31440  eulerpartlemd  31684  coinflippvt  31802  ballotth  31855  hgt750lem  31982  hgt750lem2  31983  quad3  32973  onint1  33857  bj-csbsn  34292  cnambfre  35053  sqmid3api  39411  re1m1e0m0  39469  sn-1ticom  39504  rabren3dioph  39676  arearect  40085  areaquad  40086  resnonrel  40212  cononrel1  40214  cononrel2  40215  lhe4.4ex1a  40957  expgrowthi  40961  expgrowth  40963  binomcxplemnotnn0  40984  liminf0  42365  dvcosre  42484  stoweidlem34  42606  fouriersw  42803
  Copyright terms: Public domain W3C validator