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

Theorem 3eqtr3i 2681
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 2675 . 2 𝐵 = 𝐶
4 3eqtr3i.3 . 2 𝐵 = 𝐷
53, 4eqtr3i 2675 1 𝐶 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  un12  3804  in12  3857  indif1  3904  difundi  3912  difundir  3913  difindi  3914  difindir  3915  dif32  3924  csbvarg  4036  undif1  4076  resmpt3  5485  xp0  5587  fresaunres2  6114  fvsnun1  6489  caov12  6904  caov13  6906  caov411  6908  caovdir  6910  orduniss2  7075  fparlem3  7324  fparlem4  7325  hartogslem1  8488  kmlem3  9012  cdaassen  9042  xpcdaen  9043  halfnq  9836  reclem3pr  9909  addcmpblnr  9928  ltsrpr  9936  pn0sr  9960  sqgt0sr  9965  map2psrpr  9969  negsubdii  10404  halfpm6th  11291  decmul1  11623  i4  13007  nn0opthlem1  13095  fac4  13108  imi  13941  bpoly3  14833  ef01bndlem  14958  bitsres  15242  gcdaddmlem  15292  modsubi  15823  gcdmodi  15825  numexpp1  15829  karatsuba  15839  karatsubaOLD  15840  oppgcntr  17841  frgpuplem  18231  ressmpladd  19505  ressmplmul  19506  ressmplvsca  19507  ltbwe  19520  ressply1add  19648  ressply1mul  19649  ressply1vsca  19650  sn0cld  20942  qtopres  21549  itg1addlem5  23512  cospi  24269  sincos4thpi  24310  sincos3rdpi  24313  dvlog  24442  dvlog2  24444  dvsqrt  24528  dvcnsqrt  24530  ang180lem3  24586  1cubrlem  24613  mcubic  24619  quart1lem  24627  atantayl2  24710  log2cnv  24716  log2ublem2  24719  log2ub  24721  gam1  24836  chtub  24982  bclbnd  25050  bposlem8  25061  lgsdir2lem1  25095  lgsdir2lem5  25099  2lgsoddprmlem3d  25183  ex-bc  27439  ex-gcd  27444  ipidsq  27693  ip1ilem  27809  ipdirilem  27812  ipasslem10  27822  siilem1  27834  hvmul2negi  28033  hvadd12i  28042  hvnegdii  28047  normlem1  28095  normlem9  28103  normsubi  28126  normpar2i  28141  polid2i  28142  chjassi  28473  chj12i  28509  pjoml2i  28572  hoadd12i  28764  lnophmlem2  29004  nmopcoadj2i  29089  indifundif  29482  aciunf1  29591  partfun  29603  ffsrn  29632  dpmul10  29731  dpmul1000  29735  dpadd2  29746  dpadd  29747  dpmul  29749  archirngz  29871  sqsscirc1  30082  sigaclfu2  30312  eulerpartlemd  30556  coinflippvt  30674  ballotth  30727  hgt750lem  30857  hgt750lem2  30858  quad3  31690  onint1  32573  bj-csbsn  33024  cnambfre  33588  rabren3dioph  37696  arearect  38118  areaquad  38119  resnonrel  38215  cononrel1  38217  cononrel2  38218  lhe4.4ex1a  38845  expgrowthi  38849  expgrowth  38851  binomcxplemnotnn0  38872  liminf0  40343  dvcosre  40444  stoweidlem34  40569  fouriersw  40766
  Copyright terms: Public domain W3C validator